Introduction to the Calculus of Inductive Constructions

Christine Paulin-Mohring 1, 2, *
* Auteur correspondant
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Chapitre d'ouvrage
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. 〈http://www.collegepublications.co.uk/logic/mlf/?00023〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01094195
Contributeur : Christine Paulin-Mohring <>
Soumis le : jeudi 11 décembre 2014 - 18:06:36
Dernière modification le : jeudi 11 janvier 2018 - 06:25:27
Document(s) archivé(s) le : jeudi 12 mars 2015 - 11:11:13

Fichier

CIC.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01094195, version 1

Citation

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. 〈http://www.collegepublications.co.uk/logic/mlf/?00023〉. 〈hal-01094195〉

Partager

Métriques

Consultations de la notice

264

Téléchargements de fichiers

1550