
The $\lws$calculus is a $\la$calculus with explicit substitutions introduced in~\cite{mscs01}. It satisfies the desired properties of such a calculus: step by step simulation of $\beta$, confluence on terms with metavariables and preservation of the strong normalization. It was conjectured in~\cite{mscs01} that simply typed terms of $\lws$ are strongly normalizable. This was proved in~\cite{polonovsky99} by Di Cosmo \& al by using a translation of $\lws$ into the proof nets of linear logic. We give here a direct and elementary proof of this result. The strong normalization is also proved for terms typable in Girard's second order system~F. This is a new result.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 