从 X 到 Pi：在 Pi-演算中表示经典矢列演算
计算机科学中的逻辑
2011-09-23 v1
摘要
我们研究带有配对与非阻塞输入的 Pi-演算，并定义一种使用"箭头"类型构造子的类型指派。我们将演算 X 的电路编码到该 Pi-演算的变体中，并证明所有归约（cut-消去）与可指派类型均被保持。由于 X 对 Gentzen 的演算 LK 满足 Curry-Howard 同构，这意味着 LK 中的所有证明在 Pi 中都有表示。
引用
@article{arxiv.1109.4817,
title = {From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus},
author = {Steffen van Bakel and Luca Cardelli and Maria Grazia Vigliotti},
journal= {arXiv preprint arXiv:1109.4817},
year = {2011}
}
备注
International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008