A Formulae-as-Types Interpretation of Subtractive Logic
A Formulae-as-Types Interpretation of Subtractive Logic
复制标题
减法逻辑的公式作为类型的解释
DOI：
--
复制
发表时间：
2004
影响因子：
0.7
通讯作者：
T. Crolard
中科院分区：
文献类型：
--
作者：
T. Crolard
我们提出了减法逻辑（即双直觉逻辑）的公式作为类型的解释。这个演示有两个方面：我们首先定义 λμ 演算的一个非常自然的限制，它在约简下是封闭的，并且其类型系统是经典自然演绎的建设性限制。然后我们将这个演绎系统保守地扩展到减法逻辑。从计算的角度来看，生成的演算为一流协程（一流延续的受限形式）提供了类型系统。
We present a formulae-as-types interpretation of Subtractive Logic (i.e. bi-intuitionistic logic). This presentation is two-fold: we first define a very natural restriction of the λμ-calculus which is closed under reduction and whose type system is a constructive restriction of the Classical Natural Deduction. Then we extend this deduction system conservatively to Subtractive Logic. From a computational standpoint, the resulting calculus provides a type system for first-class coroutines (a restricted form of first-class continuations).