The λ-context Calculus

Murdoch Gabbay, Stéphane Lengrand

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

We present a simple but expressive lambda-calculus whose syntax is populated by variables which behave like meta-variables. It can express both capture-avoiding and capturing substitution (instantiation). To do this requires several innovations, including a key insight in the confluence proof and a set of reduction rules which manages the complexity of a calculus of contexts over the 'vanilla' lambda-calculus in a very simple and modular way. This calculus remains extremely close in look and feel to a standard lambda-calculus with explicit substitutions, and good properties of the lambda-calculus are preserved. © 2008 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)19-35
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume196
Issue numberC
DOIs
Publication statusPublished - 22 Jan 2008

Keywords

  • calculus of explicit substitutions
  • capture-avoiding substitution
  • capturing substitution
  • confluence
  • contexts
  • instantiation
  • Lambda-calculus
  • meta-variables
  • nominal techniques

Fingerprint Dive into the research topics of 'The λ-context Calculus'. Together they form a unique fingerprint.

  • Cite this