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

13:30 - 15:00: Research Papers - Modal Types at Aurora Borealis
Chair(s): Dominique DevrieseVrije Universiteit Brussel
icfp-2019-papers13:30 - 13:52
Daniel GratzerAarhus University, Jonathan SterlingCarnegie Mellon University, Lars BirkedalAarhus University
icfp-2019-papers13:52 - 14:15
Pierre-Marie PédrotINRIA, Nicolas TabareauInria, Hans FehrmannUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris
icfp-2019-papers14:15 - 14:37
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
icfp-2019-papers14:37 - 15:00
Dominic OrchardUniversity of Kent, UK, Vilem-Benjamin LiepeltUniversity of Kent, UK, Harley D. Eades IIIAugusta University