带有列表和控制操作的按值调用 lambda 演算
计算机科学中的逻辑
2012-10-12 v1
摘要
带有控制算子的演算已被用于推理编程语言中的控制流以及解释经典证明的计算内容。为了使这些演算成为真正的编程语言，还应包含数据类型。作为迈向该方向的一步，本文定义了一个简单类型的按值调用 lambda 演算，其中包含控制算子 catch 和 throw、列表数据类型以及原始递归算子（类似于 Goedel 的 T 系统）。我们证明了该系统满足主体归约、进展性、无类型项的合流性以及良类型项的强正规化性。
引用
@article{arxiv.1210.3114,
title = {Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic},
author = {Federico Aschieri and Margherita Zorzi},
journal= {arXiv preprint arXiv:1210.3114},
year = {2012}
}
备注
In Proceedings CL&C 2012, arXiv:1210.2890