HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

Introduction to the Calculus of Inductive Constructions

Christine Paulin-Mohring 1, 2, *
* Corresponding author
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : This paper gives an introduction to the Calculus of Inductive Constructions, the formalism behind the Coq proof assistant. We present the language and the typing rules, starting with the pure functional part and then introducing the inductive declarations. We briefly discuss the properties of this language, both from the theoretical and pragmatic points of view and give examples of applications.
Document type :
Book sections
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

Contributor : Christine Paulin-Mohring Connect in order to contact the contributor
Submitted on : Thursday, December 11, 2014 - 6:06:36 PM
Last modification on : Thursday, July 8, 2021 - 3:47:02 AM
Long-term archiving on: : Thursday, March 12, 2015 - 11:11:13 AM


Files produced by the author(s)


  • HAL Id : hal-01094195, version 1


Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. Bruno Woltzenlogel Paleo; David Delahaye. All about Proofs, Proofs for All, 55, College Publications, 2015, Studies in Logic (Mathematical logic and foundations), 978-1-84890-166-7. ⟨hal-01094195⟩



Record views


Files downloads