The lambda-context calculus (extended version)

Murdoch Gabbay, Stéphane Lengrand

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)

Abstract

We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows the calculus to express both capture-avoiding and capturing substitution (instantiation). The reduction rules extend the 'vanilla' lambda-calculus in a simple and modular way and preserve the look and feel of a standard lambda-calculus with explicit substitutions. Good properties of the lambda-calculus are preserved. The LamCC is confluent, and a natural injection into the LamCC of the untyped lambda-calculus exists and preserves strong normalisation. We discuss the calculus and its design with full proofs. In the presence of the hierarchy of variables, functional binding splits into a functional abstraction ? (lambda) and a name-binder i{cyrillic} (new). We investigate how the components of this calculus interact with each other and with the reduction rules, with examples. In two more extended case studies we demonstrate how global state can be expressed, and how contexts and contextual equivalence can be naturally internalised using function application. © 2009 Elsevier Inc. All rights reserved.

Original languageEnglish
Pages (from-to)1369-1400
Number of pages32
JournalInformation and Computation
Volume207
Issue number12
DOIs
Publication statusPublished - Dec 2009

Keywords

  • Binders
  • Calculi of contexts
  • Capturing substitution
  • Explicit substitutions
  • Functional programming
  • Lambda-calculus
  • Nominal techniques

Fingerprint

Dive into the research topics of 'The lambda-context calculus (extended version)'. Together they form a unique fingerprint.

Cite this