oa Towards a New Termination Checker for the Coq Proof Assistant

Modern societies rely on software applications for performing many critical tasks. As this trend is increasing, so it is the necessity to develop cost-effective methods of writing software that ensure that essential safety and security requirements are met. In this context, dependent type theories are recently gaining adoption as a valid tool for performing formal verification of software.

The focus of this work is Coq, a proof assistant based on a dependent type theory called the Calculus of Inductive Constructions. Developed at INRIA (France) for over 20 years, it is arguably one of the most successful proof assistant to this date. It has been used in several real-world large-scale projects such as the formalization of a verification framework for the Java Virtual Machine, a proof of the Four Color Theorem, and a formally verified compiler for the C programming language (project Compcert).

Coq is both a proof assistant and a programming language. To ensure soundness of the formal verification approach, Coq imposes several conditions on the source programs. In particular, all programs written in Coq must be terminating. The current implementation of the termination checker uses syntactic criteria that are too restrictive and limiting in practice, hindering the usability of the system.

In previous work we have proposed an extension of Coq using a termination checker based on the theory of sized types and we have shown that the soundness of the approach. Furthermore, compared to syntactic criteria currently used, our approach is more powerful, easier to understand, and easier to implement, as evidenced by a prototype implementation we developed.

Our objective is to turn our prototype into an implementation of a new core theory and termination checker for Coq. We expect that the resulting system will be more efficient and easier to understand for users. Furthermore it will increase the expressive power and usability of Coq, permitting the use of formal verification on a wider range of applications.