存储算子与系统TTR的全称正类型
逻辑
2009-05-06 v1
摘要
1990年，J.L. Krivine引入了存储算子的概念，用于在“按名调用”策略中模拟“按值调用”。J.L. Krivine已经证明，利用从经典逻辑到直觉主义逻辑的Gödel翻译，我们可以在AF2类型系统中为存储算子找到一个简单类型。本文研究了TTR类型系统的∀-正类型（全称二阶量词在这些类型中正出现）和Gödel变换（经典Gödel翻译的推广）。我们通过句法方法，推广了J.L. Krivine关于这些类型和这些变换的定理。我们给出了在递归整数类型情形下这一结果的证明。
引用
@article{arxiv.0905.0550,
title = {Storage operators and forall-positive types of system TTR},
author = {Karim Nour},
journal= {arXiv preprint arXiv:0905.0550},
year = {2009}
}