The weak normalization of the simply typed λs_e-calculus

In this paper, we show the weak normalization (WN) of the simply-typed ?s_e-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the ??_e-calculus, a calculus isomorphic to ?s_e^?. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the ?s-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus ??'_e which works like ?s_e but which is closer to ?s than ??_e. For both ??_e and ??'_e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all ?s open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved.