Abstract

In this paper, we show the weak normalization of the simply-typed λse-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 . This proof is strongly influenced by Goubault-Larrecq's proof of WN for the λ σ-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus λ ω′e which works like λse but which is closer to λ σ than λωe. For both λωe and λ ω′e we prove WN for typed semi-open terms , unlike the result of Goubault-Larrecq which covered all λ σ open terms