Computer Science Logic and 8th Kurt Gödel Colloquium
René DAVID & Bruno Guillaume: Strong normalization of the typed $\lambda_{ws}$- calculus
 Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions
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 meta-variables 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.