A Substructural Type System for Delimited Continuations
A Substructural Type System for Delimited Continuations
复制标题
用于定界延续的子结构类型系统
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Chung
中科院分区：
文献类型：
--
作者：
O. Kiselyov;Chung
我们提出的类型系统，抽象地解释小步，而不是大步的操作语义。我们将表达式或求值上下文视为具有假设推理的线性逻辑中的结构。求值顺序不仅由操作语义中常见的聚焦规则来规定，而且由类型系统中的结构规则来表示，使类型更紧密地跟踪控制流。绑定上下文和求值上下文是相关的，但后者是线性的。
我们使用这些思想来为分隔的延续构建一个类型系统。它允许控制操作员改变答案类型或在最近的动态封闭的边界之外行动，但不需要额外的判断和箭头类型字段来记录答案类型。直接风格程序的类型派生将其转换为延续传递风格。
We propose type systems that abstractly interpret small-step rather than big-step operational semantics. We treat an expression or evaluation context as a structure in a linear logic with hypothetical reasoning. Evaluation order is not only regulated by familiar focusing rules in the operational semantics, but also expressed by structural rules in the type system, so the types track control flow more closely. Binding and evaluation contexts are related, but the latter are linear.
We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a directstyle program desugars it into continuation-passing style.