Hostname: page-component-745bb68f8f-grxwn Total loading time: 0 Render date: 2025-01-13T13:00:20.807Z Has data issue: false hasContentIssue false
  • English
  • Français

Modular proof of strong normalization for the calculus of constructions

Published online by Cambridge University Press:  10 August 2016

Herman Geuvers  and
Mark-Jan Nederhof
Herman Geuvers
Affiliation:
Faculty of Mathematics and Computer Science, University of Nijmegen, The Netherlands
Mark-Jan Nederhof
Affiliation:
Faculty of Mathematics and Computer Science, University of Nijmegen, The Netherlands
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We present a modular proof of strong normalization for the Calculus of Constructions of Coquand and Huet (1985, 1988). This result was first proved by Coquand (1986), but our proof is more perspicious. The method consists of a little juggling with some systems in the cube of Barendregt (1989), which provides a fine structure of the calculus of constructions. It is proved that the strong normalization of the calculus of constructions is equivalent with the strong normalization of Fω.

In order to give the proof, we first establish some properties of various type systems. Therefore, we present a general framework of typed lambda calculi, including many well-known ones.

Type
Research Article
Information
Journal of Functional Programming , Volume 1 , Issue 2 , April 1991 , pp. 155 - 189
Copyright
Copyright © Cambridge University Press 1991

References

Barendregt, H. P. 1984. The Lambda calculus, its syntax and semantics, North Holland.Google Scholar
Barendregt, H. P. 1989. Introduction to generalised type systems. Proc. 3rd Italian Conference on Theoretical Computer Science, World Scientific Publishing Co., Singapore.Google Scholar
Barendregt, H. P. 1990. Lambda calculi with types. In Abramsky, S., Gabbai, D. M. and Maibaum, T. S. E. (editors), Handbook of Logic in Computer Science. Oxford University Press.Google Scholar
Barendregt, H. P. and Dekkers, W. 1990. Typed Lambda Calculi.Google Scholar
Barendsen, E. 1989. Representation of logic, data types and recursive functions in typed lambda calculi. Masters Thesis, Faculty of Mathematics and Computer Science, University of Nijmegen, The Netherlands.Google Scholar
Berardi, S. 1988. Towards a mathematical analysis of type dependence in Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Department of Computer Science, CMU, and Dipartimento di Matematica, Torino.Google Scholar
de Bruijn, N. G. 1980. A survey of the project AUTOMATH. In Hindley, J. R. and Seldin, J. P. (editors), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 579–606. Academic Press.Google Scholar
Church, A. 1940. A formulation of the simple theory of types. Journal of Symbolic Logic, 5: 56–68.CrossRefGoogle Scholar
Coquand, T. 1986. Metamathematical Investigations of a Calculus of Constructions, INRIA, France and Cambridge University, UK.Google Scholar
Coquand, T. and Huet, G. 1985. Constructions: a higher order proof system for mechanizing mathematics. In Buchberger, B. (editor), EUROCAL 85. Volume 203 of Lecture Notes in Computer Science, pp. 151–184.Google Scholar
Coquand, T. and Huet, G. 1988. The calculus of constructions. In Meyer, A. R. (editors), Information and Computation, pp. 95–120.Google Scholar
Geuvers, H. 1988. The interpretation of logics in type systems. Masters Thesis, Faculty of Mathematics and Computer Science, Catholic University Nijmegen, The Netherlands.Google Scholar
Girard, J.-Y. 1972. Interpretation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de Doctorat d'Etat, Université de Paris VIII, France.Google Scholar
Girard, J.-Y. 1971. Une extension de l'interprétation de Gödei à l'analyse, et son application a l'élimination des coupures dans l'analyse et la theorie des types. In Fenstad, J. E. (editor), Proceedings of the second Scandinavian Logic Symposium. North Holland.Google Scholar
Harper, R., Honsell, F. and Plotkin, G. 1987. A framework for defining logics. Proc. Symposium on Logic in Computer Science, Ithaca, New York, IEEE, Washington.Google Scholar
Howard, W. 1980. The formulae-as-types notion of construction. In Hindley, J. R. and Seldin, J. P. (editors), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490.Google Scholar
Luo, Z. 1988. and its strong normalization. Notes of a talk given at the Jumelage meeting on typed Lambda Calculus, Nijmegen, The Netherlands.Google Scholar
Tait, W. W. 1967. Intensional interpretation of functions of finite type. Journal of Symbolic Logic, 32: 198–212.Google Scholar
Tait, W. W. 1975. A realizability interpretation of the theory of species. In Parikh, R. (editor), Logic Colloquium. Volume 453 of Lecture Notes in Mathematics, pp. 240–51. Springer-Verlag.Google Scholar
Terlouw, J. 1989a. Een nadere bewijstheoretische analyse van GSTT's. Internal report, Faculty of Mathematics and Computer Science, University of Nijmegen, The Netherlands.Google Scholar
Terlouw, J. 1989b. Sterke normalisatie in C à la Tait. Notes of a lecture held at the Intercity Seminar Typed Lambda Calculus, Nijmegen, The Netherlands.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.