Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Implementing a modal dependent type theory
Gratzer D., Sterling J., Birkedal L.  Proceedings of the ACM on Programming Languages 3 (ICFP): 1-29, 2019. Type: Article
Date Reviewed: Apr 27 2021

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.

Reviewer:  Temur Kutsia Review #: CR147252
Bookmark and Share
General (D.3.0 )
Proof Theory (F.4.1 ... )
Type Structure (F.3.3 ... )
General (F.0 )
Would you recommend this review?
Other reviews under "General": Date
 The kollected Kode Vicious: opinionated advice for programmers
Neville-Neil G.,  Addison-Wesley, Boston, MA, 2020. 311 pp. Type: Book (978-1-367882-46-1)
Apr 30 2021
Environmental bisimulations for probabilistic higher-order languages
Sangiorgi D., Vignudelli V.  ACM Transactions on Programming Languages and Systems 41(4): 1-64, 2019. Type: Article
Feb 2 2021
Learning programming languages as shortcuts to natural language token replacements
Barmpoutis A.  Koli Calling 2018 (Proceedings of the 18th Koli Calling International Conference on Computing Education Research, Koli, Finland,  Nov 22-25, 2018) 1-10, 2018. Type: Proceedings
Nov 3 2020

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2021 ThinkLoud, Inc.
Terms of Use
| Privacy Policy