A typed context calculus

Masatomo Hashimoto, Atsushi Ohori

Research output: Contribution to journalArticlepeer-review

16 Citations (Scopus)


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 languageEnglish
Pages (from-to)249-272
Number of pages24
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 2001 Sept 6
Externally publishedYes


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this