The Weak Normalization of the Simply Typed {lambda}se-calculus

In this paper, we show the weak normalization (WN) of the simply-typeds_e-calculus with open terms where abstractions are decoratedwith types, and metavariables, de Bruijn indices and updatingoperators are decorated with environments. We show a proof ofWN using the _e-calculus, a calculus isomorphic to . This proof is strongly influenced by Goubault-Larrecq'sproof of WN for the -calculus but with subtle differences whichshow that the two styles require different attention. Furthermore,we give a new calculus '_e which works like s_e but which iscloser to than _e. For both _e and '_e we prove WN for typedsemi-open terms (i.e. those which allow term variables but nosubstitution variables), unlike the result of Goubault-Larrecqwhich covered all open terms.