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

This paper extends the Dijkstra monad framework, designed to write specifcations over effectful programs using monadic effects, to handle termination sensitive specifications over interactive programs. We achieve this by introducing base specification monads for non-terminating programs with uninterpreted events. We model such programs using Interaction Trees, a coinductive model for modelling programs with algebraic effects in Coq, which we further develop by adding trace semantics to achieve our goals. We also show that this approach subsumes typical, simple proof principles. We implement the framework as an extension of the Interaction Trees Coq library.

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 Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas Silver University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet Rajani MPI-SP, Marco Gaboardi Boston University, Deepak Garg Max Planck Institute for Software Systems, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam Choudhury University of Pennsylvania, Harley D. Eades III Augusta University, Richard A. Eisenberg Tweag I/O, Stephanie Weirich University of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron Moy Northeastern University, Phúc C. Nguyễn Google, Sam Tobin-Hochstadt Indiana University, David Van Horn University 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 Cockx TU Delft, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N
Link to publication DOI Pre-print