交叉类型与 Lambda 理论
计算机科学中的逻辑
2007-05-23 v1
摘要
我们阐述了将交叉类型作为语义工具来证明 lambda 理论格性质的用法。基于简单交叉类型理论的概念，我们成功构建了一个过滤器模型，在该模型中，任意简单 easy 项的解释是任何能通过谓词以统一方式描述的过滤器。这使我们能够证明一个著名的 lambda 理论的一致性：该一致性对 lambda 理论格的代数结构具有有趣的推论。
引用
@article{arxiv.cs/0211011,
title = {Intersection Types and Lambda Theories},
author = {M. Dezani-Ciancaglini and S. Lusin},
journal= {arXiv preprint arXiv:cs/0211011},
year = {2007}
}