A formulae-as-type notion of control
A formulae-as-type notion of control
复制标题
公式作为类型的控制概念
DOI：
--
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
T. Griffin
中科院分区：
文献类型：
--
作者：
T. Griffin
编程语言Scheme包含控制结构call/cc，它允许访问当前continuation（当前控制上下文）。这实际上为Scheme提供了一流的标签和跳转。我们证明了著名的公式作为类型的对应关系，它将公式α的构造性证明与类型α的程序联系起来，可以扩展到类型化的理想概型。令人惊讶的是，这种对应关系将经典证明与类型化程序联系起来。计算上有趣的“经典程序”的存在-α型程序，其中α保持经典，但不是建设性的-通过使用标准经典定义定义的合取，析取和存在类型的定义来说明。我们还证明了理想化概型中所有类型项的求值都是有限的。
The programming language Scheme contains the control construct call/cc that allows access to the current continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as-types correspondence, which relates a constructive proof of a formula α to a program of type α, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting “classical programs” —programs of type α, where α holds classically, but not constructively — is illustrated by the definition of conjunctively, disjunctive, and existential types using standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.