Skip to main content
SpringerLink
Log in

Extensions of pure type systems

  • Conference paper
  • First Online:
Book cover Typed Lambda Calculi and Applications (TLCA 1995)

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

Included in the following conference series:

Abstract

We extend pure type systems with quotient types and subset types and establish an equivalence between four strong normalisation problems: subset types, quotient types, definitions and the so-called K-rules. As a corollary, we get strong normalisation of ECC with definitions, subset and quotient types.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barendregt. Typed λ-calculi, Handbook of logic in computer science, Abramsky and al eds, OUP 1992.

    Google Scholar 

  2. G. Barthe. Towards a mathematical vernacular, submitted.

    Google Scholar 

  3. G. Barthe. Formalizing mathematics in type theory: fundamentals and case studies, submitted.

    Google Scholar 

  4. G. Barthe. An introduction to quotient and congruence types, manuscript, University of Nijmegen, November 1994.

    Google Scholar 

  5. R. Constable and al. Implementing Mathematics with the NuPrl Proof Development System, Prenctice Hall, 1986.

    Google Scholar 

  6. T. Coquand. A new paradox in type theory, in the proceedings of the 9th Congress of Logic, Methodology and Philosophy of Science.

    Google Scholar 

  7. H. Geuvers. Logics and type systems, Ph.D thesis, University of Nijmegen, 1993.

    Google Scholar 

  8. H. Geuvers. A short and flexible proof of strong normalisation for the Calculus of Constructions, submitted.

    Google Scholar 

  9. M. Hofmann. Extensional concepts in intensional type theory, Ph.D thesis, University of Edinburgh, forthcoming.

    Google Scholar 

  10. M. Hofmann. A simple model for quotient types, in these proceedings.

    Google Scholar 

  11. B. Jacobs. Categorical Logic and Type Theory, in preparation.

    Google Scholar 

  12. B. Jacobs. Quotients in simple Type Theory, submitted.

    Google Scholar 

  13. J. Lambek and P.J. Scott. Introduction to higher-order categorical logic, CUP, 1986.

    Google Scholar 

  14. Z. Luo. Computation and reasoning: a type theory for computer science, OUP, 1994.

    Google Scholar 

  15. N. Mendler. Quotient types via coequalisers in Martin-Lof's type theory, in the informal proceedings of the workshop on logical frameworks, Antibes, May 1990.

    Google Scholar 

  16. R. Nederpelt and al (eds). Selected Papers on Automath, North-Holland, 1994.

    Google Scholar 

  17. B. Nordstrom, K. Petersson and J. Smith. Programming in Martin-Lof's type theory, OUP, 1990.

    Google Scholar 

  18. E. Poll and P. Severi. PTS with definitions, in proceedings of LFCS'94, LNCS 813.

    Google Scholar 

  19. G. Pottinger. Definite descriptions and excluded middle in the theory of constructions, TYPES mailing list, November 1989.

    Google Scholar 

  20. A. Salvesen and J. Smith. The strength of the subset type in Martin-Lof's type theory, proceedings of LICS'88, 1988.

    Google Scholar 

  21. J. Terlouw. Strong normalisation in type systems: a model-theoretical approach, Dirk van Dalen Festschrift, Utrecht, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics and Informatics, University of Nijmegen, The Netherlands

    Gilles Barthe

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mariangiola Dezani-Ciancaglini Gordon Plotkin

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G. (1995). Extensions of pure type systems. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014042

Download citation

  • DOI: https://doi.org/10.1007/BFb0014042

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59048-4

  • Online ISBN: 978-3-540-49178-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation