Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
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 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:20
Interaction and ApplicationsTyDe at Aurora Borealis
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford
09:00
20m
Talk
Flexible Structure Editing of Well-Typed Expressions
TyDe
David Moon, Cyrus OmarUniversity of Chicago, Ben ShapiroUniversity of Colorado, Boulder
Pre-print
09:20
20m
Talk
Livelits: Filling Typed Holes with Live GUIs
TyDe
Cyrus OmarUniversity of Chicago, Nick CollinsUniversity of Chicago, David Moon, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago
Pre-print
09:40
20m
Talk
Formal Investigation of the Extended UTxO Model
TyDe
Orestis MelkonianUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
10:00
20m
Talk
An Algebra of Sequential Decision Problems
TyDe
Robert KrookChalmers University of Technology, Patrik JanssonChalmers University of Technology
Pre-print