Modalities are widely used in mathematics and computer science as an abstraction tool, but it turns out to be difficult to incorporate them in rich type theories. The authors address this problem, proposing a new dependent type theory MLTT_🔒 that integrates an S4-style necessity modality □ into the standard Martin-Löf type theory. The goal of this integration is to develop a powerful computational and logical framework, which, as it is stated in the paper, “can be used simultaneously as a basis for next-generation programming languages and as a metalanguage for synthetic mathematics.”

In type theories, type checking is a fundamental problem. At its core, there is the problem of deciding equality between types. For dependent types, this task involves the equality check between terms as well. A well-known approach to the latter is based on normalization by evaluation (NbE), reducing terms to a canonical representation in their equivalence class.

The authors developed and investigated these techniques for MLTT_🔒. NbE is extended to deal with modalities and is proved to be sound and complete. (For reasons of space, the paper does not contain the full proof and the reader is referred to the accompanying technical report, but the latter is not cited.) It is used in the design of a type checking algorithm for a version of MLTT_🔒 with suitable type annotations. Type checking in this version is decidable. The algorithm is shown to be sound and complete.

One may wonder why the lock symbol 🔒 appears in the name of MLTT_🔒. It is related to the locking operation, used to make variables inaccessible it applies to (instead of dropping them) in the process of proving. Locked contexts may later get unlocked, thus making the locked variables accessible again. These operations are used in rules that handle □: To prove □ A, one may lock the context and continue with proving A. On the other hand, it is possible to unlock the locked context to switch to proving □ A from proving A.

After developing the (technically quite involved) theoretical part, the authors illustrate the practicality of their approach, providing an implementation of a prototype proof assistant based on the calculus.

I think that researchers working in type theory, logical frameworks, proof assistant systems, and dependently typed programming will appreciate this work. Directions for future investigations, provided at the end of the paper, look interesting.