Lambda Mu 演算与对偶性：按名调用与按值调用
逻辑
2007-06-13 v1
摘要
在 Curry-Howard 对应扩展到经典逻辑的框架下，Gentzen 的 NK 和 LK 系统可分别视为 Parigot 的 Lambda Mu 演算和 Curien-Herbelin 的 Lambda Bar Mu Mu Tilde 演算的简单类型语法导向系统。我们旨在展示它们的计算等价性。我们定义了这些演算之间的翻译。我们证明了针对无向求值以及按名调用和按值调用求值的模拟定理。
引用
@article{arxiv.0706.1728,
title = {Lambda Mu Calculus and Duality: Call-by-Name and Call-by-Value},
author = {Jérôme Rocheteau},
journal= {arXiv preprint arXiv:0706.1728},
year = {2007}
}