Untyped Call-by-Value Calculus with First-Class Continuations and Environments
Untyped Call-by-Value Calculus with First-Class Continuations and Environments
复制标题
具有一流延续和环境的非类型化值调用演算
DOI：
10.1142/9789813279674_0008
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
S. Nishizaki
中科院分区：
文献类型：
--
作者：
Yuta Aoyagi;S. Nishizaki
在编程语言中，一级对象是一个实体，它可以作为实际参数传递给函数，并作为返回值从函数返回。你可以从一级对象的角度对编程语言进行分类和比较。延续意味着程序中某个点的剩余计算，它对应于编程语言处理器中的调用堆栈。环境是变量名到绑定值的映射。在lambda演算的框架下，Felleisen研究了第一类连续，我们研究了第一类环境，本文提出了一种具有第一类连续和第一类环境的按值调用lambda演算。它的操作语义形式化为一个小的步骤语义使用评估上下文。然后，我们显示的稳健性属性的操作语义与第一类延续和记录的调用的值lambda演算。
In programming languages, first-class object is an entity which can be passed to a function as an actual parameter and returned from the function as a return value. You can classify and compare the programming languages from the point of view of first-class object. A continuation means a rest of computation at some point in a program, which corresponds to a call stack in a programming language processor. An environment is a mapping of variable names to bound values. In the framework of the lambda calculus, the first-class continuation was studied by Felleisen and the first-class environment has been studied by us.In this paper, we propose a call-by-value lambda calculus with first-class continuations and environment. Its operational semantics is formalized as a small-step semantics using evaluation contexts. Then, we show the soundness property of the operational semantics with respect to the call-by-value lambda calculus with first-class continuations and records.