Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Cubical Agda: a dependently typed programming language with univalence and higher inductive types
Vezzosi A., Mörtberg A., Abel A.  Proceedings of the ACM on Programming Languages 3 (ICFP): 1-29, 2019. Type: Article
Date Reviewed: Jul 23 2021

Russell proposed type theory in the first decades of the 20th century in response to the foundational crisis faced by set theory. Over the last century, there have been a number of developments in type theory, in particular the mechanization of type theory exemplified in tools like Isabelle, Coq, and Agda. There have been some notable successes of mechanization both in the field of mathematics (the proof of Kepler’s conjecture) and in computer science (a formally verified compiler, CompCert).

Over the last decade, a new variant of type theory--homotopy type theory (HoTT)--has come to the forefront, providing fine-grained analysis of one of the most important and subtle aspects of logic: equality. It achieves this by importing concepts from homotopy theory. The double payoff is in the new perspectives it provides: for mathematicians, the computational and constructive aspects of type theory; and for computer scientists, the ability to automate and simplify reasoning about equality.

The current paper explains the implementation of a variant of HoTT--cubical HoTT--that minimizes axioms in the theory by introducing an “interval type.” The interval type allows expressing and reasoning about homotopy between functions, directly in the theory instead of the meta-theory, thereby providing a more efficient mechanization of the theory. The paper also shows how features indispensable for a proof assistant, such as pattern matching, can be incorporated in the presence of HoTT constructs such as higher inductive types. The end result is a fully fledged proof assistant for HoTT.

HoTT has generated quite a bit of excitement in foundational maths and in computer science (CS). I am reminded of the situation in the last two decades of the 20th century: monads and their application to programming language semantics--that too was a result of importing some fundamental structures from mathematics into CS, with a deep and lasting impact on the practice of CS. Some of the applications from the formalization of HoTT in Agda are quite exciting; for example, a mechanization of the mathematics of “patches” mentioned in the future work section is intriguing!

I also expect to see HoTT applied to program specification and refinement. The difference this time around--in comparison with monads--is that HoTT will hopefully also have a deep and lasting impact on the practice of mathematics: Agda and other similar mechanizations of HoTT could provide nontrivial assistance to mathematicians in their day-to-day work, as well as make cutting-edge mathematics more accessible by encapsulating it into shrink-wrapped software.

Reviewer:  Prahladavaradan Sampath Review #: CR147316 (2112-0289)
Bookmark and Share
General (D.2.0 )
General (D.3.0 )
General (F.0 )
Would you recommend this review?
Other reviews under "General": Date
 Code that fits in your head : heuristics for software engineering
Seeman M.,  Pearson, Hoboken, NJ, 2021. 406 pp. Type: Book (978-1-374644-01-4)
May 27 2022
 Code that fits in your head: heuristics for software engineering
Seemann M.,  Addison-Wesley Professional, Boston, MA, 2021. 416 pp. Type: Book (978-0-137464-40-1)
May 23 2022
Open tools for software engineering: validation of a theory of openness in the automotive industry
Munir H., Runeson P., Wnuk K.  EASE 2019 (Proceedings of the Evaluation and Assessment on Software Engineering, Copenhagen, Denmark,  Apr 15-17, 2019) 2-11, 2019. Type: Proceedings
Jul 29 2021

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