The Calculus of Inductive Constructions (CIC) is the formalism on which the Coq proof assistant is based. It is a dependently-typed calculus with inductive types 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).

Induction-recursion [Dybjer2] is an extension of the framework of inductive types [Dybjer1,CP] with mutual definition of recursive functions over the inductive type being built. One one side, induction-recursion significantly increases the logical expressiveness of the meta-theory [], but, more importantly from a practical point of view, it allows elegant formalizations of various data structures [McBride].

The objective of the internship is to express the induction-recursion framework on top of the CIC and to provide an effective implementation of it in the Coq proof assistant.

Bibliography

• [CP] Thierry Coquand, Christine Paulin-Mohring, Inductively defined types, Proceedings of Colog’88, LNCS, 1988.
• [Dybjer1] Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65(2), 2000.
• [Dybjer2] Peter Dybjer, Inductive Families, Formal Aspects of Computation. 6(4), 1994.
• [McBride] Conor McBride, Dependently-Typed Metaprogramming 5/8: Induction-Recursion I and II, online video lectures, 2013.
• [Setzer] Anton Setzer, Extending Martin-Löf Type Theory by one Mahlo-universe, Archive of Mathematical Logic. 39(3), 2000.

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