Skip to main content
SpringerLink
Log in

The Not So Simple Proof-Irrelevant Model of CC

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2646))

Included in the following conference series:

Abstract

It is well-known that the Calculus of Constructions (CC) bears a simple set-theoretical model in which proof-terms are mapped onto a single object—a property which is known as proof-irrelevance. In this paper, we show that when going into the (generally omitted) technical details, this naive model raises several unexpected difficulties related to the interpretation of the impredicative level, especially for the soundness property which is surprisingly difficult to be given a correct proof in this simple framework. We propose a way to tackle these difficulties, thus giving a (more) detailed elementary consistency proof of CC without going back to a translation to F ω . We also discuss some possible alternatives and possible extensions of our construction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Aczel. On relating type theories and set theories, in Types for Proofs and Programs, edited by Altenkirch, Naraschewski and Reus, Proceedings of Types’ 98, LNCS 1657 (1999).

    Chapter  Google Scholar 

  2. T. Altenkirch. Extensional Equality in Intensional Type Theory. In Proceedings of the fourteenth Annual IEEE Symposium on Logic in Computer Science, IEEE, 1999.

    Google Scholar 

  3. H. Barendregt. Lambda Calculi with Types. Technical Report 91-19, Catholic University Nijmegen, 1991. In Handbook of Logic in Computer Science, Vol II, Elsevier, 1992.

    Google Scholar 

  4. F. Barbanera, S. Berardi. Proof-irrelevance out of Excluded Middle and Choice in the Calculus of Constructions. Journal of Functional Programming, vol. 6(3), 519–525, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  5. B. Barras and B. Werner. Coq in Coq. Manuscript.

    Google Scholar 

  6. G. Barthe. Domain-free pure type systems. Journal of Functional Programming, vol. 10(5), p. 412–452, 2000.

    Article  MathSciNet  Google Scholar 

  7. L. Chicli, L. Pottier and C. Simpson. Quotient Types in Coq. Presentation at the TYPES’01 Workshop, Nijmegen, 2001.

    Google Scholar 

  8. Th. Coquand. Une Théorie des Constructions. Thèse de Doctorat, Université Paris 7, janvier 1985.

    Google Scholar 

  9. Th. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Oddifredi (editor), Logic and Computer Science. Academic Press, 1990. Rapport de recherche INRIA 1088.

    Google Scholar 

  10. Th. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2/3), 1988.

    Google Scholar 

  11. H. Geuvers. Logics and Type Systems. PhD Thesis, Katholieke Universiteit Nijmegen, 1993.

    Google Scholar 

  12. J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, Thèse d’État, Université Paris 7, 1972.

    Google Scholar 

  13. J.-Y. Girard. Translation and appendices Y. Lafont and P. Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.

    Google Scholar 

  14. J.-L. Krivine. Théorie des ensembles. Cassini, Paris, 1998.

    MATH  Google Scholar 

  15. P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory, Bibliopolis, 1984.

    Google Scholar 

  16. J. McKinna and R. Pollack. Pure Type Systems formalized, in TLCA’93, M. Bezem and J. F. Groote Eds, LNCS 664, Springer-Verlag, Berlin, 1993.

    Google Scholar 

  17. P.-A. Melliès and B. Werner. A Generic Normalization Proof for Pure Type Systems. In TYPES’96, E. Gimenez and C. Paulin-Mohring Eds, LNCS 1512, Springer-Verlag, Berlin, 1998.

    Google Scholar 

  18. A. Miquel. A Model for Impredicative Type Systems with Universes, Intersection Types and Subtyping. Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS’00), 2000.

    Google Scholar 

  19. A. Miquel. Le calcul des constructions implicite: syntaxe et sémantique. Thèse de doctorat, Université Paris 7, 2001.

    Google Scholar 

  20. J. Reynolds. Polymorphism is not Set-Theoretic, Semantics of Data Types G. Kahn, D. B. MacQueen and G. Plotkin Eds. LNCS 173, pp. 145–156, Springer-Verlag, Berlin, 1984.

    Google Scholar 

  21. T. Streicher. Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhaeuser Verlag, Basel 1991.

    Google Scholar 

  22. B. Werner. Sets in Types, Types in Sets. In, M. Abadi and T. Itoh (Eds), Theoretical Aspects of Computer Science, TACS’97, LNCS 1281, Springer-Verlag, 1997.

    Chapter  Google Scholar 

  23. B. Werner. Une Théorie des Constructions Inductives. Thèse de Doctorat, Université Paris 7, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire de Recherche en Informatique, Université Paris-Sud, F - 91405, ORSAY cedex, France

    Alexandre Miquel

  2. INRIA-Rocquencourt, BP 105, F - 78 1 53, LE CHESNAY cedex, France

    Benjamin Werner

Authors
  1. Alexandre Miquel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin Werner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Nijmegen, Toernooiveld 1, 6525 ED, Nijmegen, The Netherlands

    Herman Geuvers  & Freek Wiedijk  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Miquel, A., Werner, B. (2003). The Not So Simple Proof-Irrelevant Model of CC. In: Geuvers, H., Wiedijk, F. (eds) Types for Proofs and Programs. TYPES 2002. Lecture Notes in Computer Science, vol 2646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39185-1_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-39185-1_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-14031-3

  • Online ISBN: 978-3-540-39185-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation