Explicit Substitutions and Reducibility
Hugo Herbelin · Journal of Logic and Computation · 2001
We consider reducibility sets defined not by induction on types but by induction on sequents as a tool to prove strong normalization of systems with explicit substitution. To illustrate this point, we give a proof of strong normalization (SN) for simply‐typed call‐by‐name λ̄μμ̃‐calculus enriched with operators of explicit unary substitutions. The λ̄μμ̃‐calculus, defined by Curien and Herbelin, is a variant of λμ‐calculus with a let operator that exhibits symmetries such as terms/contexts and call‐by‐name/call‐by‐value reduction.