A Filter Model for the λμ-Calculus - (Extended Abstract)
A Filter Model for the λμ-Calculus - (Extended Abstract)
复制标题
λμ 微积分的滤波器模型 -（扩展摘要）
DOI：
10.1007/978-3-642-21691-6_18
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Ugo de'Liguoro
中科院分区：
文献类型：
--
作者：
S. V. Bakel;Franco Barbanera;Ugo de'Liguoro
介绍了纯λμ微积分的一个交点型分配系统，该系统在主题约简和展开式下是不变的。利用Abramsky的域逻辑方法描述了Streicher和Reus在-代数格范畴内的延拓表示模型，得到了该系统。这提供了一个工具，可以通过过滤器模型构造显示类型分配系统相对于延续模型的完整性。我们还证明了Parigot系统中类型化的λμ项在我们的系统中具有非平凡交类型化。
We introduce an intersection type assignment system for the pure λμ- calculus, which 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 ω-algebraic lattices via Abramsky's domain logic approach. This provides a tool for showing the completeness of the type assignment sys- tem with respect to the continuation models via a filter model construction. We also show that typed λμ-terms in Parigot's system have a non-trivial intersection typing in our system.