Reimplementing Dependent Pattern Matching and Termination Checking in the Coq Theorem Prover

Coq is an interactive proof assistant (theorem prover) based on a long-studied dependent Type Theory called the Calculus of (Co-)Inductive Constructions (CIC). It is a mature system that has been used in large-scale projects including formalization of mathematical theories (e.g., Four-Color Theorem) and program verification (e.g., formal verification of a C compiler). It is also used in several universities around the world as a tool for teaching courses on topics such as programming languages, formal verification, and logic. However, despite its success, some limitations in CIC hinder the development of specifications in Coq. In previous work, we targeted some of these limitations in the termination checker and pattern matching mechanisms of Coq. We have proposed extensions of CIC that increase the expressiveness of the system, are more intuitive for users, and have the potential of increasing the efficiency of Coq. Furthermore, we have proved that these extensions preserve fundamental properties of a proof assistant based on dependent types such as decidability of type-checking and logical consistency. The objective in this proposed project is to turn these theoretical results into a practical implementation. Specifically, we propose to reimplement the kernel of Coq to incorporate the extensions we have developed. This will increase the expressive power and usability of Coq, and help to bring it to a wider range of applications and users.