mitten: A Flexible Multimodal Proof Assistant
Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. In this talk we focus on one such type theory, MTT: a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints. These modalities are specified by mode theories, 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities.
We contribute a defunctionalized NbE algorithm which reduces the type checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories—mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type checking algorithm. We further contribute
Mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20
|mitten: A Flexible Multimodal Proof AssistantRemote|
|Understandable and Useful Error Messages for Liquid TypesRemote|
Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
|Deciding type equivalence with simple grammarsIn-Person|
|Typechecking up to CongruenceIn-Person|
Jad Elkhaleq Ghalayini University of Cambridge
|À bas l’η — Coq’s troublesome η-conversionRemote|
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes