From Lambda-sigma to Lambda-upsilon a Journey Through Calculi of Explicit Substitutions

Abstract

This paper gives a systematic description of several calculi of explicit substitutions. These systems are orthogonal and have easy proofs of termination of their substitution calculus. The last system, called λv, entails a very simple environment machine for strong normalization of λ-terms.