Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 3, pp. 431-451: Abstract.

Explicit Substitutions and Reducibility

Hugo Herbelin

É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

  Full-Text PDF  (222 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.