传名调用演算的二值传递CPS变换

摘要：

为Plotkin带常数传名调用(演算定义了一个新的CPS(continuation-passing-style)变换方法.方法基于求值上下文变换,新颖之处在于,每次传递二值给继续而不是常规的一值.先给出二值CPS变换编码,再在此基础上定义CPS语言,最后建立源语言和CPS语言的一一映射关系并证明Plotkin的模拟定理.与Plotkin的工作比较,工作特点在于,给出了一个CPS归约闭语言,该语言中所有继续都可以用函数形式表达,且模拟定理的可靠性和完备性方向证明更为简单.

关键词：程序演算、形式语义、传名调用、CPS(continuation-passing-style)、归约

所属期刊栏目：19

分类号：TP301(计算技术、计算机技术)

资助基金：the National Natural Science Foundation of China under Grant Nos.60496321, 60673045

在线出版日期：2008-12-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：2508-2516