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 Bruijn-numbers, 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.
CITATION STYLE
Ritter, E., & De Paiva, V. (1997). On explicit substitutions and names. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1256, pp. 248–258). Springer Verlag. https://doi.org/10.1007/3-540-63165-8_182
Mendeley helps you to discover research relevant for your work.