Abstract
λσ-calculus is an extended λ-calculus where substitutions are handled explicity. We prove the strong normalization of its subcalculus σ which computes substitutions.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit Substitutions. Journal of Functional Programming, to appear.
P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. 1991. Submitted.
P.-L. Curien, T. Hardin, and A. Ríos. Normalisation Forte du Calcul des Substitutions. Technical Report, LIENS-Ecole Normale Supérieure, 1991.
P.-L. Curien. Categorical Combinators, Sequential Algotithms and Computer Science. Pitman, 1986.
T. Hardin. Confluence Results for the Pure Strong Categorical Logic CCL: λ-calculi as Subsystems of CCL. Theoretical Computer Science, 65(2), 1989.
T. Hardin and A. Laville. Proof of Termination of the Rewriting System SUBST on CCL. Theoretical Computer Science, 46, 1986.
M. Sleep. Issues for implementing lambda languages. Notes for Ustica Workshop, September 1985.
J. Staples. A Graph-like Lambda-Calculus for which leftmost-outermost reduction is optimal. In Claus, editor, Graph Grammars and their Applications to Computer Science and Biology, Springer-Verlag, 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curien, P.L., Hardin, T., Ríos, A. (1992). Strong normalization of substitutions. In: Havel, I.M., Koubek, V. (eds) Mathematical Foundations of Computer Science 1992. MFCS 1992. Lecture Notes in Computer Science, vol 629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55808-X_19
Download citation
DOI: https://doi.org/10.1007/3-540-55808-X_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55808-8
Online ISBN: 978-3-540-47291-9
eBook Packages: Springer Book Archive