Implementing a modal dependent type theory
Abstract
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 theoryMLTT🔒supporting the connectives of standard Martin-Löf Type Theory as well as anS4-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 forMLTT🔒, using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant forMLTT🔒, demonstrating the ease of applying our techniques.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jul 26, 2019
- Source ID
- 10.1145/3341711
Entities
People
- Daniel Gratzer
- Jonathan Sterling
- Lars Birkedal
Organizations
- Aarhus University
- Air Force Office of Scientific Research
- Carnegie Mellon University
- Natural Sciences, Danish Council for Independent Research
- Villum Foundation