Let-Binding in a Linear Lambda Calculus with First-Class Continuations

2018 4th International Conference on Environmental Science and Material Application

生态环境科学;材料科学

Nishizaki, Shinya^1

Department of Computer Science Tokyo, Institute of Technology Tokyo, Japan^1

关键词: Lambda calculus;    Linear lambda calculus;    Type systems;    Value reduction;   

Others  :  https://iopscience.iop.org/article/10.1088/1755-1315/252/4/042011/pdf
DOI  :  10.1088/1755-1315/252/4/042011

来源: IOP

【 摘 要 】

In our previous work, we proposed a linear lambda calculus with first-class continuations. In the usual lambda calculus, an argument value can be duplicated and deleted, but the continuation cannot. In our calculus, a value is allowed to be neither duplicated nor deleted, but a continuation is allowed, so it can be considered to be dual with the usual lambda calculus. In this paper, we extend a linear lambda calculus with first-class continuations by adding let-binding. We define a syntax, a call-by-value reduction, and a type system of the calculus. Then, we discuss the let-polymorphism in our calculus.