Context-based proofs of termination for typed delimited-control operators
Context-based proofs of termination for typed delimited-control operators
复制标题
类型化分隔控制运算符的基于上下文的终止证明
DOI：
10.1145/1599410.1599446
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Dariusz Biernacki
中科院分区：
文献类型：
--
作者：
Małgorzata Biernacka;Dariusz Biernacki
我们给出了使用基于上下文的可约简谓词的Tait方法的变体来直接证明类型化定界控制运算符移位和重置的求值终止。我们既处理按值调用和按名称调用，对于每个缩减策略，我们认为类型和效果系统类似于Danvy和Filinski，以及具有固定应答类型的系统。我们提出的按值调用类型和效果系统是对Danvy和Filinski原始类型系统的改进，而按名称调用类型和效果系统是新的。从规范化证明中，我们提取了具有两层延续的连续传递风格的按值调用和按名称调用赋值器；通过构造，这些赋值器是按赋值规范化的实例。
We present direct proofs of termination of evaluation for typed delimited-control operators shift and reset using a variant of Tait's method with context-based reducibility predicates. We address both call by value and call by name, and for each reduction strategy we consider a type-and-effect system a la Danvy and Filinski as well as a system with a fixed answer type. The call-by-value type-and-effect system we present is a refinement of Danvy and Filinski's original type system, whereas the call-by-name type-and-effect system is new. From the normalization proofs, we extract call-by-value and call-by-name evaluators in continuation-passing style with two layers of continuations; by construction, these evaluators are instances of normalization by evaluation.