Abstract
The Λ-calculus has been much used to study the theory of substitution in logical systems and programming languages. However, with explicit substitutions, it is possible to get finer properties with respect to gradual implementations of substitutions as effectively done in runtimes of programming languages. But the theory of explicit substitutions has some defects such as non-confluence or the non-termination of the typed case. In this paper, we stress on the sub-theory of weak substitutions, which is sufficient to analyze most of the properties of programming languages, and which preserves many of the nice theorems of the Λ-calculus. © Springer-Verlag Berlin Heidelberg 1999.
Cite
CITATION STYLE
Lévy, J. J., & Maranget, L. (1999). Explicit substitutions and programming languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1738, pp. 181–200). Springer Verlag. https://doi.org/10.1007/3-540-46691-6_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
