X 演算中的归约与交并类型不相容（扩展摘要）
计算机科学中的逻辑
2011-09-22 v1
摘要
本文定义了 X 演算的交类型与并类型赋值。X 演算是一种无替换语言，与 Gentzen 经典逻辑相继式演算具有 Curry-Howard 对应关系。我们证明了该类型赋值在主题扩张下是封闭的，并指出需要对其加以限制才能满足主题归约，这使得它不适合用于定义语义。
引用
@article{arxiv.1109.4570,
title = {Reduction in X does not agree with Intersection and Union Types (Extended abstract)},
author = {Steffen van Bakel},
journal= {arXiv preprint arXiv:1109.4570},
year = {2011}
}
备注
4th International Workshop on Intersection Types and Related Systems (ITRS'08), Turin, Italy, March 2008