存储算子的一般类型
A General Type for Storage Operators
摘要:
1990年,J.L. Krivine在$λ$ -演算中引入了存储操作符的概念来模拟“按名称调用”上下文中的“按值调用”。J.L. Krivine已经证明,使用从经典逻辑到直觉主义逻辑的哥德尔翻译,我们可以在AF 2型系统中找到一个简单的存储算子类型。本文给出了存储算子在AF ~ 2的一个小扩张中的一般类型。我们在最后(没有证明)给出了这个结果的推广到其他类型。
英文摘要:
In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $λ$-calculus, the "call by value" in a context of a "call by name". J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this result to other types.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。