A typed context calculus

Masatomo Hashimoto, Atsushi Ohori

Research output: Contribution to journalArticle

27 Citations (Scopus)

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

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