Skip to main content
SpringerLink
Log in

A generic normalisation proof for pure type systems

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

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

Included in the following conference series:

Abstract

We prove the strong normalisation for any PTS, provided the existence of a certain Λ-set \(\mathfrak{A}^ \Uparrow \) (s) for every sort s of the system. The properties verified by the \(\mathfrak{A}^ \Uparrow \) (s)’s depend of the axiom and rules of the type system.

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. T. Altenkirch. Constructions, Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh, 1993.

    Google Scholar 

  2. H. Barendregt. Lambda Calculi with Types. In Handbook of Logic in Computer Science, Vol II, Elsevier, 1992

    Google Scholar 

  3. G. Barthe, P.-A. Melliès. On the Subject Reduction property for algebraic type systems. In Proceedings CSL'96, LNCS 1258, Springer Verlag, 1996.

    Google Scholar 

  4. G. Dowek, G. Huet and B. Werner. On the Definition of the η-long Normal Form in Type Systems of the Cube. Submitted to publication. See also http://pauillac.inria.fr/~werner/,1996.

    Google Scholar 

  5. H. Geuvers et M.-J. Nederhof. A modular proof of strong normalization for the Calculus of Constructions. Journal of Functional Programming, 1 (2):155–189, 1991.

    MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  7. J. W. Klop, Combinatory Reduction Systems. Ph.D. Thesis, Utrecht University, 1980.

    Google Scholar 

  8. G. Longo and E. Moggi. Constructive Natural Deduction and its ω-set Interpretation.

    Google Scholar 

  9. Z. Luo. An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh, 1990.

    Google Scholar 

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

    Google Scholar 

  11. W. W. Tait. A realizability interpretation of the theory of species. In Logic Colloquium, R. Parikh Ed. LNM 453, Springer-Verlag, 1975.

    Google Scholar 

  12. J. Terlouw. Strong Normalization in Type Systems: a model theoretical approach. In Dirk van Dalen Festschrift, Henk Barendregt, Marc Bezem and Jan Willem Klop Eds. Dept. of Philosophy, Utrecht University, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Edinburgh, James Clerk Maxwell Building, EH9 3JZ, Edinburgh, Scotland

    Paul-André Melliès & Benjamin Werner

  2. INRIA-Rocquencourt, BP 105, F-78 153, Lechesnay cedex, France

    Paul-André Melliès & Benjamin Werner

Authors
  1. Paul-André Melliès
    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

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Melliès, PA., Werner, B. (1998). A generic normalisation proof for pure type systems. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097796

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65137-6

  • Online ISBN: 978-3-540-49562-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation