| Explicit Substitutions and Reducibility (2001) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. We consider reducibility sets dened 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, dened by Curien & Herbelin, is a variant of -calculus with a let operator that exhibits symmetries such as terms/contexts and call-byname /call-by-value reduction. The ~-calculus embeds various standard -calculi (and Gentzen's style sequent calculi too) and as an application we derive the strong normalization of Parigot's simply-typed -calculus with explicit substitution. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||