The λ_(ωs)-calculus is a λ-calculus with explicit substitutions introduced in [4]. It satisfies the desired properties of such a calculus: step by step simulation of β, confluence on terms with meta-variables and preservation of the strong normalization. It was conjectured in [4] that simply typed terms of λ_(ωs) are strongly normalizable. This was proved in [7] by Di Cosmo & al. by using a translation of λ_(ωs) 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 with second order types (the extension of Girard's system F). this is a new result.
展开▼
机译：λ_（ωs）-calculululululululcululululululululululululululululululululululululululululululululum，其中[4]中引入了明确的替换。它满足这种微分的所需性质：逐步模拟β，汇率与元变量的术语，并保存强归一化。它在[4]中猜测，简单地键入的λ_（ωs）的术语是强烈归一定的。 DI Cosmo＆Al证明了这一点[7]。通过使用λ_（ωs）的转换为线性逻辑的证明网。我们在这里提供直接和基本证明这一结果。对于具有二阶类型的术语，还证明了强烈的正常化（Girard系统F的延伸）。这是一个新的结果。
展开▼
