一句话：为 lambda-mu 演算建立对规约与展开不变的交集类型系统，并用滤模型证明相对续延模型的完备性及强规范化刻画。
本文为 lambda-mu 演算引入交集类型系统，并使其在主体归约与主体展开下保持不变。系统构造基于 Abramsky 的 domain logic 方法，用以描述 Streicher 与 Reus 在 omega-代数格范畴中的续延指称模型；通过滤模型构造，既给出类型解释，也证明系统相对续延模型的完备性。随后定义限制系统，使 lambda-mu 项可类型化当且仅当强规范化。作者还将 Parigot 用经典有效命题公式对 lambda-mu 项的类型指派翻译到限制系统，从而为带类型 lambda-mu 演算的强规范化提供新证明。
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambda-mu terms with classically valid propositional formulas can be translated into the restricted system, which then provides an alternative proof of strong normalisability for the typed lambda-mu calculus.
@article{paperbot438,
title = {Intersection Types for the lambda-mu Calculus},
author = {Steffen van Bakel and Franco Barbanera and Ugo de'Liguoro},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:2)2018}
}