期刊
THEORETICAL COMPUTER SCIENCE
卷 266, 期 1-2, 页码 249-272出版社
ELSEVIER SCIENCE BV
DOI: 10.1016/S0304-3975(00)00174-2
关键词
context; lambda-calculus; type system; alpha-renaming
This paper develops a typed calculus for contexts i.e., lambda terms with holes. In addition to ordinary lambda terms, the calculus contains labeled holes, hole abstraction and context application for manipulating first-class contexts. The primary operation for contexts is hole-filling, which captures free variables. This operation conflicts with substitution of the lambda calculus, and a straightforward mixture of the two results in an inconsistent system. We solve this problem by defining a type system that precisely specifies the variable-capturing nature of contexts and that keeps track of bound variable renaming. These mechanisms enable us to define a reduction system that properly integrates beta -reduction and hole-filling. The resulting calculus is Church-Rosser and the type system has the subject reduction property. We believe that the context calculus will serve as a basis for developing a programming language with advanced features that call for manipulation of open terms. (C) 2001 Elsevier Science B.V. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据