The Calculus of Inductive Constructions (CIC) is the formalism on which the Coq proof assistant is based. It is a dependently-typed calculus which is both a programming language and a logical system and it can be seen as an impredicative extension of Martin-Löf’s Intensional Type Theory (ITT). In ITT, formulae/types are considered up to evaluation of proofs/programs dependent in types. This induces an intensional equality which is decidable and hence suitable for implementation.

Constrastingly, Extensional Type Theory (ETT) is a variant of ITT in which formulae/types are considered up to extensional equality of programs. This induces a stronger notion of equality which is natural for reasoning but which has some drawbacks on decidability. Not only it is not itself decidable (what can be addressed by giving explicit proofs of equality, as done in the Nuprl implementation of a variant of ETT [Nuprl]), but it also allows to type non-normalizing terms.

The objective of the internship is first to provide with an abstract presentation of CIC with an extensional equality, somehow related to the approach followed in [CAC], then to restrict extensionality so as to support any arbitrary equality inbetween intensional and extensional equality, then to investigate one particular such subset, namely the one built from those equality schemes that are provable in a unique way and without axioms.

The interest in this latter sub-extensional notion of equality is that, while being undecidable like extensional equality, it presumably does not allow to type non-normalizing terms as soon as the underlying intensional type theory does not.

Not to loose decidability of equality, the trick is to keep computationally transparent proof witnesses as done in [PTSF] for preserving the computational transparency of intensional type theory in a context with no conversion at all. It will be part of the objectives of the internship to investigate this approach, after what the main property that normalization is preserved will have to be addressed.

Possible extra questions are: what are the exact subsets of FunExt and UIP that are validated by this theory; what subsets of the considered equality can be taken in charge by a decidable algorithm for equality; how to implement this mixed intensional-extensional theory?

Bibliography

• [CAC] Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada, The Calculus of Algebraic Constructions, in Proceedings of Rewriting Techniques and Applications, LNCS 1631, 2006.
• [Hofmann] Martin Hofmann, Extensional concepts in intensional type theory, PhD thesis, 1995.
• [HoTT] The HoTT Book on Homotopy type theory, 2013.
• [Nuprl] The NuPRL project.
• [PTSF] Floris van Doorn, Herman Geuvers, Freek Wiedijk, Explicit Convertibility Proofs in Pure Type Systems, in Proceedings of LFMTP 2013, the Eighth ACM SIGPLAN international workshop on Logical frameworks and meta-languages: theory and practice, Boston USA, September 2013, ACM (digital library).

This document was translated from L^AT_EX by H^EV^EA.