Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Implementing a modal dependent type theory
Gratzer D., Sterling J., Birkedal L. Proceedings of the ACM on Programming Languages3 (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 (2108-0213)
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?
yes
no
Other reviews under "General": Date
Programming languages: paradigm and practice
Appleby D., McGraw-Hill, Inc., New York, NY, 1991. Type: Book (9780075579045)
Jan 1 1992
Programming languages
Dershem H. (ed), Jipping M., Wadsworth Publ. Co., Belmont, CA, 1990. Type: Book (9780534129002)
Jan 1 1992
Comparative programming languages
Friedman L., Prentice-Hall, Inc., Upper Saddle River, NJ, 1991. Type: Book (9780131554825)
Jan 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy