Skip to main content
SpringerLink
Log in

Proving strong normalization of CC by modifying realizability semantics

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

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

Included in the following conference series:

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. Thorsten Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993.

    Google Scholar 

  2. Thorsten Altenkirch. Yet another strong normalization proof for the Calculus of Constructions. In Proceedings of El Vintermöte, number 73 in Programming Methodology Group Reports. Chalmers University, Göteborg, 1993.

    Google Scholar 

  3. H.P. Barendregt. The Lambda Calculus — Its Syntax and Semantics (Revised Edition). Studies in Logic and the Foundations of Mathematics. North Holland, 1984.

    Google Scholar 

  4. H.P. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, Vol. 2, pages 118–310. Oxford University Press, 1992.

    Google Scholar 

  5. Thierry Coquand and Jean Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. Informal Proceedings of the First Annual Workshop on Logical Frameworks, Antibes, 1990.

    Google Scholar 

  6. Thierry Coquand and Gerard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

    Article  Google Scholar 

  7. Thierry Coquand. Une théorie des constructions. PhD thesis, Université Paris VII, 1985.

    Google Scholar 

  8. Thomas Ehrhard. Dictoses. In D.H. Pitt et al., editors, Category Theory and Computer Science, pages 213–223. Springer, 1989. LNCS 389.

    Google Scholar 

  9. Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.

    Google Scholar 

  10. J.M.E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In J.F. Groote M. Bezem, editor, Typed Lambda Calculi and Applications, LNCS 664, 1993.

    Google Scholar 

  11. Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. LFCS report ECS-LFCS-92-208, University of Edinburgh, 1992.

    Google Scholar 

  12. Thomas Streicher. Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. PhD thesis, Universität Passau, Passau, West Germany, June 1989.

    Google Scholar 

  13. Thomas Streicher. Semantics of Type Theory. Birkhäuser, 1991.

    Google Scholar 

  14. Benjamin Werner. A normalization proof for an impredicative type system with large eliminations over integers. In Workshop on Logical Frameworks. BRA Types, 1992. Preliminary Proceedings.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Chalmers University of Technology, 412 64, Gothenburg, Sweden

    Thorsten Altenkirch

Authors
  1. Thorsten Altenkirch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Henk Barendregt Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Altenkirch, T. (1994). Proving strong normalization of CC by modifying realizability semantics. In: Barendregt, H., Nipkow, T. (eds) Types for Proofs and Programs. TYPES 1993. Lecture Notes in Computer Science, vol 806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58085-9_70

Download citation

  • DOI: https://doi.org/10.1007/3-540-58085-9_70

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58085-0

  • Online ISBN: 978-3-540-48440-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation