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.

• Type: Conference
• Year: 1999
• Where: FSTTCS
• Authors: Jean-Jacques Lévy, Luc Maranget
• Keywords: Explicit Substitutions, FSTTCS 1999, Logical Systems, Programming Languages, Software Engineering