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.