Explicit Substitutions and Programming Languages

13 years 7 months ago
Explicit Substitutions and Programming Languages
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.
Jean-Jacques Lévy, Luc Maranget
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Authors Jean-Jacques Lévy, Luc Maranget
Comments (0)