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 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.