Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 13:30 - 13:52 at Aurora Borealis - Modal Types Chair(s): Dominique Devriese

Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theory $\mathsf{MLTT}{\mathsf{lock}}$ supporting the connectives of standard Martin-L{"o}f Type Theory as well as an S4-style necessity operator. $\mathsf{MLTT}{\mathsf{lock}}$ supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type-checking algorithm for $\mathsf{MLTT}{\mathsf{lock}}$, using a novel extension of normalization-by-evaluation. We have also implemented our algorithm in a prototype proof assistant for $\mathsf{MLTT}{\mathsf{lock}}$, demonstrating the ease of applying our techniques.

Wed 21 Aug

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

13:30 - 15:00
Modal TypesResearch Papers at Aurora Borealis
Chair(s): Dominique Devriese Vrije Universiteit Brussel
13:30
22m
Talk
Implementing a Modal Dependent Type TheoryDistinguished Paper
Research Papers
Daniel Gratzer Aarhus University, Jonathan Sterling Carnegie Mellon University, Lars Birkedal Aarhus University
13:52
22m
Talk
A Reasonably Exceptional Type Theory
Research Papers
Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria, Hans Fehrmann University of Chile, Éric Tanter University of Chile & Inria Paris
14:15
22m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Research Papers
Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
14:37
22m
Talk
Quantitative program reasoning with graded modal types
Research Papers
Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK, Harley D. Eades III Augusta University
Pre-print