Abstract | ||
---|---|---|
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&brg;-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. Copyright 2001 Elsevier Science B.V. |
Year | DOI | Venue |
---|---|---|
2001 | 10.1016/S0304-3975(00)00174-2 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
Type system,lambda calculus,fi-renaming,ordinary lambda term,context calculus,subject reduction property,reduction system,context application,first-class context,Lambda-calculus,inconsistent system,Context,Alpha-renaming,context,lambda term,type system | Journal | 266 |
Issue | ISSN | Citations |
1-2 | Theoretical Computer Science | 26 |
PageRank | References | Authors |
1.14 | 12 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Masatomo Hashimoto | 1 | 68 | 5.97 |
Atsushi Ohori | 2 | 26 | 1.14 |