### 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 β-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.

Original language | English |
---|---|

Pages (from-to) | 249-272 |

Number of pages | 24 |

Journal | Theoretical Computer Science |

Volume | 266 |

Issue number | 1-2 |

DOIs | |

Publication status | Published - 2001 Sep 6 |

Externally published | Yes |

### Keywords

- Alpha-renaming
- Context
- Lambda-calculus
- Type system

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'A typed context calculus'. Together they form a unique fingerprint.

## Cite this

*Theoretical Computer Science*,

*266*(1-2), 249-272. https://doi.org/10.1016/S0304-3975(00)00174-2