Abstract
Calculi with explicit substitutions have found widespread acceptance as a basis for abstract machines for functional languages. In this paper we investigate the relations between variants with de Bruijnnumbers, with variable names, with reduction based on raw expressions and calculi with equational judgements. We show the equivalence between these variants, which is crucial in establishing the correspondence between the semantics of the calculus and its implementations.
Research supported under the EPSRC project no. GR/L28296, x-SLAM: The Explicit Substitutions Linear Abstract Machine.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
R. Bloo and K.H. Rose. Preesrvation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In Proc. CSN'95 — Computer Science in the Netherlands, pages 62–72, 1995.
C. Coquand. From semantics to rules: A machine assisted analysis. In CSL'93, volume 832 of LNCS, 1994.
P.-L. Curien, Th. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43:362–397, March 1996.
Pierre-Louis Curien, An abstract framework for environment machines (Note). Theoretical Computer Science, 82(2):389–402, 1991.
Herman Geuvers. Logics and Type Systems. PhD thesis, Univ. of Nijmegen, 1993.
Thérèse Hardin. Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCL. Theoretical Computer Science, 65:291–342, 1989.
F. Kamareddine and A. Rios. A lambda-calculus a la de bruijn with explicit substitutions. In PLILP'95, volume 982 of LNCS, 1995.
P. Lescanne. From λσ to λυ: a journey through calculi of explicit substitutions. POPL'94, pages 60–69, Portland, Oregon, 1994.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
P.-A. Mellies. Typed λ-calculi with explicit substitution may not terminate. TLCA'95, pages 328–334. LNCS No. 902, 1995.
E. Ritter and V. de Paiva. On explicit substitution and names. Technical report, Univ. of Birmingham, School of Computer Science, 1997.
Eike Ritter. Normalization for typed lambda calculi with explicit substitution. CSL'93, pages 295–304. LNCS No. 832, 1994.
Thomas Streicher. Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. PhD thesis, Universität Passau, June 1989.
A. Tasistro. Formulation of Martin-Löf's theory types with explicit substitutions. Licenciate Thesis, Chalmers University, Dept. of Computer Science, May 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ritter, E., de Paiva, V. (1997). On explicit substitutions and names (extended abstract). In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds) Automata, Languages and Programming. ICALP 1997. Lecture Notes in Computer Science, vol 1256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63165-8_182
Download citation
DOI: https://doi.org/10.1007/3-540-63165-8_182
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63165-1
Online ISBN: 978-3-540-69194-5
eBook Packages: Springer Book Archive