Journal of Logic and Computation, Volume 11, Issue 3, pp. 431451: Abstract.
Explicit Substitutions and ReducibilityHugo Herbelin^{} ^{}Équipe LogiCal, INRIARocquencourt, BP105, 78153 Le Chesnay Cedex, France. Email: 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 simplytyped callbyname [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 callbyname/callbyvalue reduction.
Keywords: Calculus, strong normalization, reducibility, explicit substitutions
