ICFP 2019 (series) / TyDe 2019 (series) / TyDe 2019 /
Formal Investigation of the Extended UTxO Model
Sun 18 Aug 2019 09:40 - 10:00 at Aurora Borealis - Interaction and Applications Chair(s): Jeremy Gibbons
We formulate an accounting model for ledgers based on unspent transaction outputs (UTxO), the ledger model underlying Bitcoin and many other blockchains. We conduct our study in Agda, exploiting its expressive dependent type system to mechanically enforce desired properties statically.
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 18 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:20 | Interaction and ApplicationsTyDe at Aurora Borealis Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
09:00 20mTalk | Flexible Structure Editing of Well-Typed Expressions TyDe Pre-print | ||
09:20 20mTalk | Livelits: Filling Typed Holes with Live GUIs TyDe Cyrus Omar University of Chicago, Nick Collins University of Chicago, David Moon , Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago Pre-print | ||
09:40 20mTalk | Formal Investigation of the Extended UTxO Model TyDe Orestis Melkonian Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK Pre-print | ||
10:00 20mTalk | An Algebra of Sequential Decision Problems TyDe Pre-print | ||