|
|
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
 | |
Print this page