Journal of Logic and Computation, Volume 11, Issue 3, pp. 431-451: Abstract.
Explicit Substitutions and Reducibility
Équipe LogiCal, INRIA-Rocquencourt, BP105, 78153 Le Chesnay Cedex, France. E-mail: Hugo.Herbelin@inria.fr
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 [lambda] ¯[mu][mu] [tilde]-calculus enriched with operators of explicit unary substitutions. The [lambda] ¯[mu][mu] [tilde]-calculus, defined by Curien and Herbelin, is a variant of [lambda][mu]-calculus with a let operator that exhibits symmetries such as terms/contexts and call-by-name/call-by-value reduction.
Keywords: Calculus, strong normalization, reducibility, explicit substitutions