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
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
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.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian