This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Th. Altenkirch, Yet another Strong Normalization proof for the Calculus of Constructions, Laboratory for Foundations of Computer Science, Manuscript, 11 pp.
Th. Altenkirch, Constructions, Inductive types and Strong Normalization proof, Ph. D. Thesis, University of Edinburgh, UK.
F. Barbanera, M. Fernández, J.H. Geuvers, Modularity of Strong Normalization in the lambda-algebraic-cube, manuscript.
H.P. Barendregt, The lambda calculus: its syntax and semantics, revised edition. Studies in Logic and the Foundations of Mathematics, North Holland.
H.P. Barendregt, Typed lambda calculi. In Abramski et al. (eds.), Handbook of Logic in Computer Science, Oxford Univ. Press.
S. Berardi, Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Dept. Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, Italy.
Th. Coquand, Une théorie des constructions, Thèse de troisième cycle, Université Paris VII, France.
Th. Coquand, Metamathematical investigations of a calculus of constructions. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 91–122.
Th. Coquand and J. Gallier, A proof of Strong Normalization for the Theory of Constructions using a Kripke-like interpretation, In the Informal Proceedings of the Workshop on Logical Frameworks, Antibes, May 1990.
Th. Coquand and G. Huet, The calculus of constructions, Information and Computation, 76, pp 95–120.
Th. Coquand and Ch. Paulin-Mohring Inductively defined types, In P. Martin-Löf and G. Mints editors. COLOG-88: International conference on computer logic, LNCS 411.
J.H. Geuvers and M.J. Nederhof, A modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, vol 1 (2), pp 155–189.
J.H. Geuvers, Logics and Type Systems, Ph. D. thesis, Universiteit Nijmegen, the Netherlands.
H. Geuvers and B. Werner, On the Church-Rosser property for Expressive Type Systems and its Consequences for their Metatheoretic Study, in Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society, pp 320–329.
On Girard's “Candidats de Reductibilité”. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 123–204.
J.-Y. Girard, Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Ph.D. thesis, Université Paris VII, France.
J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Camb. Tracts in Theoretical Computer Science 7, Cambridge University Press.
H. Goguen, A Typed Operational Semantics for Type Theory, PhD. thesis, University of Edinburgh, UK, 1994.
Z. Luo, An Extended Calculus of Constructions, Ph. D. Thesis, University of Edinburgh, UK.
Z. Luo, ECC: An extended Calculus of Constructions. Proc. of the fourth ann. symp. on Logic in Comp. Science, Asilomar, Cal. IEEE, pp 386–395.
P. Martin-Löf, Intuitionistic Type Theory, Studies in Proof theory, Bibliopolis, Napoli.
B. Nordström, K. Petersson, J.M. Smith, Programming in Martin-Löf's Type Theory. Oxford University Press.
L. Ong and E. Ritter, A generic Strong Normalization argument: application to the Calculus of Constructions, University of Cambridge Computer Laboratory, Manuscript, 19 pp.
A guide to polymorphic types. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 387–420.
W.W. Tait, Infinitely long terms of transfinite type. In Formal Systems and Recursive Functions, eds. J.N. Crossley and M.A.E. Dummett, North-Holland.
W.W. Tait, A realizability interpretation of the theory of species. In Proceedings of Logic Colloquium, ed. R. Parikh, LNM 453, pp 240–251.
J. Terlouw, Strong Normalization in type systems: a model theoretic approach, In the Dirk van Dalen Festschrift, Eds. H. Barendregt, M. Bezem and J.W. Klop, Department of Philosophy, Utrecht University, the Netherlands, pp 161–190.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geuvers, H. (1995). A short and flexible proof of strong normalization for the calculus of constructions. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_2
Download citation
DOI: https://doi.org/10.1007/3-540-60579-7_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60579-9
Online ISBN: 978-3-540-47770-9
eBook Packages: Springer Book Archive