Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus
Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus
复制标题
线性使用的效果：Monadic 和 CPS 变换为线性 Lambda 演算
DOI：
10.1007/3-540-45788-7_10
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Masahito Hasegawa
中科院分区：
文献类型：
--
作者：
Masahito Hasegawa
通过给出计算lambda演算(被认为是类型化按值调用编程语言的核心演算)到线性lambda演算的一元变换，我们提出了一个用于模拟线性使用效果的语义和语法框架。作为一个例子，Berdine等人关于线性使用的延拓的S的工作可以放在这个总体图中。作为一个技术结果，我们证明了CPS变换到线性Lambda演算的完全完备性。
We propose a semantic and syntactic framework for modelling linearly used effects, by giving the monadic transforms of the computational lambda calculus (considered as the core calculus of typed call-by-value programming languages) into the linear lambda calculus. As an instance Berdine et al.'s work on linearly used continuations can be put in this general picture. As a technical result we show the full completeness of the CPS transform into the linear lambda calculus.