On the Role of Type Decorations in the Calculus of Inductive Constructions

  • Bruno Barras
  • Benjamin Grégoire
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


In proof systems like Coq [16], proof-checking involves comparing types modulo β-conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also erased. It generalizes and strengthens significantly a similar result by Barthe and Sørensen [5] on the class of functional Domain-free Pure Type Systems.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aspinall, D., Compagnoni, A.: Subtyping dependent types. Theor. Comput. Sci. 266(1-2), 273–309 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Barendregt, H.: Lambda calculi with types. In: Abramsky, Gabbay, Maibaum (eds.) Handbook of Logic in Computer Science, vol. 2, Clarendon, Oxford (1992)Google Scholar
  3. 3.
    Barras, B.: Auto-validation d’un système de preuves avec familles inductives. PhD thesis, Université Paris 7 (1999)Google Scholar
  4. 4.
    Barthe, G., Coquand, T.: On the equational theory of non-normalizing pure type systems. Journal of Functional Programming 14(2), 191–209 (2004)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Barthe, G., Sørensen, M.: Domain-free pure type systems. Journal of Functional Programming 10(5), 412–452 (2000)CrossRefGoogle Scholar
  6. 6.
    Boutin, S.: Using reflection to build efficient and certified decision procedures. In: TACS, pp. 515–529 (1997)Google Scholar
  7. 7.
    Castagna, G., Chen, G.: Dependent types with subtyping and late-bound overloading. INFCTRL: Information and Computation (formerly Information and Control), 168 (2001)Google Scholar
  8. 8.
    Chen, G.: Subtyping calculus of construction. In: Privara, I., Ružička, P. (eds.) MFCS 1997. LNCS, vol. 1295, Springer, Heidelberg (1997)CrossRefGoogle Scholar
  9. 9.
    Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235–246. ACM Press, New York (2002)Google Scholar
  10. 10.
    Leroy, X., Doligez, J.V.D.: The Objective Caml System. Institut National de Recherche en Informatique et en Automatique, Software and documentation (August 2004), Available on the Web
  11. 11.
    Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)Google Scholar
  12. 12.
    McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3-4) (November 1999)Google Scholar
  13. 13.
    Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. Ph.d. thesis, Paris 7 (January 1989)Google Scholar
  14. 14.
    Pollack, R.: The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Univ. of Edinburgh (1994)Google Scholar
  15. 15.
    Streicher, T.: Semantics of Type Theory: Correctness, Completeness, and Independence Results. Birkhauser (1991)Google Scholar
  16. 16.
    The Coq development team. The coq proof assistant reference manual v7.2. Technical Report 255, INRIA, France, march (2002),
  17. 17.
    Werner, B.: Une Théorie de Constructions Inductives. Ph.d. thesis, Université Paris 7 (May 1994) Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Bruno Barras
    • 1
  • Benjamin Grégoire
    • 2
  1. 1.INRIA FutursFrance
  2. 2.INRIA Sophia-AntipolisFrance

Personalised recommendations