Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 18:30 - 18:40 at POPL-B - Types and Proof Assistance

We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within them, namely, by decoupling the execution of operation calls into signalling that an operation’s implementation needs to be executed, and interrupting a running computation with the operation’s result, to which the computation can react by installing interrupt handlers. We formalise these ideas in a small core calculus, called λæ. We demonstrate the flexibility of λæ using examples ranging from a multi-party web application, to preemptive multi-threading, to remote function calls, to a parallel variant of runners of algebraic effects. In addition, the paper is accompanied by a formalisation of λæ’s type safety proofs in Agda, and a prototype implementation of λæ in OCaml.

Conference Day
Wed 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Types and Proof AssistancePOPL at POPL-B
18:30
10m
Talk
Asynchronous Effects
POPL
Danel AhmanUniversity of Ljubljana, Matija PretnarUniversity of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas SilverUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet RajaniMPI-SP, Marco GaboardiBoston University, Deepak GargMax Planck Institute for Software Systems, Jan HoffmannCarnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam ChoudhuryUniversity of Pennsylvania, Harley D. Eades IIIAugusta University, Richard A. EisenbergTweag I/O, Stephanie WeirichUniversity of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron MoyNortheastern University, Phúc C. NguyễnGoogle, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland, USA
Link to publication DOI Pre-print
19:20
10m
Talk
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Jesper CockxTU Delft, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Pre-print