Abstract
In this paper strong normalization is proved for terms of systems obtained by combining strong normalizing algebraic term rewriting systems with the Calculus of Constructions. The proof of the main result exploits the observation that the proof of strong normalization for the Calculus of Constructions given by Geuvers and Nederhof partly applies to this calculus extended with algebraic rewriting.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
F.Barbanera. Combining term rewriting and type assignment systems. Proceedings Third Italian Conference on Theoretical Computer Science. pp.71–84. Mantova.Bertoni, Boehm, Miglioli Eds. Nov. 1989.
Val Breazu-Tannen, Jan Gallier. Polymorphic rewriting conserves algebraic strong normalization. To appear in TCS.
T. Coquand, G. Huet. The Calculus of Constructions. Information and Control, pp.76–95, 120, 1988.
M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Functional character of solvable terms. Zeit.Math.Logik und Grund.Math. 27, pp.45–58, 1981.
H.Geuvers, M.J.Nederhof. A simple modular proof of the strong nonnalization for the Calculus of Constructions. To appear in "Journal of Functional Programming".
R. Harper, F. Honsell, G. Plotkin. A framework for defining logics. Proceedings of the symposium on Logic in Computer Science. Ithaca, New York, IEEE, Washinton D.C. 1987.
G.Pottinger. A type assignment for the strongly normalizable λ-terms. In To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic press, pp.561–578, 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbanera, F. (1991). Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_96
Download citation
DOI: https://doi.org/10.1007/3-540-54317-1_96
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54317-6
Online ISBN: 978-3-540-47558-3
eBook Packages: Springer Book Archive