Reference. 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. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 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.
Cite
Cited by (1)
Strange new universes: Proof assistants and synthetic foundations shulman-2024-strange
Existing computer programs called proof assistants can verify the correctness of mathematical proofs but their specialized proof languages present a barrier to entry for many mathematicians. Large language models have the potential to lower this barrier, enabling mathematicians to interact with proof assistants in a more familiar vernacular. Among other advantages, this may allow mathematicians to explore radically new kinds of mathematics using an LLM-powered proof assistant to train their intuitions as well as ensure their arguments are correct. Existing proof assistants have already played this role for fields such as homotopy type theory.
Cites 20 works (4 here)
With notes (4)
A Stratified Approach to Löb Induction gratzer-2022-a
Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories. Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.
Multimodal Dependent Type Theory gratzerNutyzBirkedal2021
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.
Implementing a modal dependent type theory gratzer-2019-implementing
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 MLTT 🔒 supporting the connectives of standard Martin-Löf Type Theory as well as an S4 -style necessity operator. MLTT 🔒 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 MLTT 🔒 , using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant for MLTT 🔒 , demonstrating the ease of applying our techniques.
First steps in synthetic guarded domain theory: step-indexing in the topos of trees birkedalFirstStepsSGDT2012
We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S. Moreover, we give an axiomatic categorical treatment of models of synthetic guarded domain theory and prove that, for any complete Heyting algebra A with a well-founded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S.
External (16)
- Greatest hits: Higher inductive types in coinductive definitions via induction under clocks (2022)
- Sikkel: Multimode simple type theory as an agda library (2022)
- Normalization for multimodal type theory (2022)
- An investigation of kripke-style modal type theories (2022)
- Modal dependent type theory and dependent right adjoints (2020)
- Multimodal dependent type theory (2020)
- Formalizing π-calculus in guarded cubical agda (2020)
- Simply ratt: A fitch-style modal calculus for reactive programming without space leaks (2019)
- Bisimulation as path type for guarded recursive types (2019)
- Internal Universes in Models of Homotopy Type Theory (2018)
- The clocks are ticking: No more delays! (2017)
- A Fibrational Framework for Substructural and Modal Logics (2017)
- Adjoint Logic with a 2-Category of Modes (2016)
- Programming and reasoning with guarded recursion for coinductive types (2015)
- Normalization by Evaluation: Dependent Types and Impredicativity (2013)
- An algorithm for type-checking dependent types (1996)