TY - JOUR

T1 - A typed context calculus

AU - Hashimoto, Masatomo

AU - Ohori, Atsushi

N1 - Funding Information:
∗Corresponding author. E-mail address: masatomo@is.s.u-tokyo.ac.jp (M. Hashimoto). 1Current aAliation: Department of Information Science, University of Tokyo, Bunkyo-ku, Tokyo 113-0033, Japan. 2Current aAliation: School of Information Science, Japan Advanced Institute of Science and Technology, Tatsunokuchi, Ishikawa 923-1291, Japan. Atsushi Ohori’s work was partly supported by the Japanese Ministry of Education Grant-in-Aid for Scienti2c Research on Priority Area no. 275: “Advanced databases”, and by the Parallel and Distributed Processing Research Consortium, Japan.

PY - 2001/9/6

Y1 - 2001/9/6

N2 - 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 β-reduction and hole-filling. The resulting calculus is Church-Rosser and the type systehas 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.

AB - 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 β-reduction and hole-filling. The resulting calculus is Church-Rosser and the type systehas 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.

KW - Alpha-renaming

KW - Context

KW - Lambda-calculus

KW - Type system

UR - http://www.scopus.com/inward/record.url?scp=0035817845&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0035817845&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(00)00174-2

DO - 10.1016/S0304-3975(00)00174-2

M3 - Article

AN - SCOPUS:0035817845

VL - 266

SP - 249

EP - 272

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -