The λ-context Calculus

Murdoch Gabbay; Stéphane Lengrand

doi:10.1016/j.entcs.2007.09.015

The λ-context Calculus

Murdoch Gabbay
, Stéphane Lengrand

Research output: Contribution to journal › Article › peer-review

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 language	English
Pages (from-to)	19-35
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	196
Issue number	C
DOIs	https://doi.org/10.1016/j.entcs.2007.09.015
Publication status	Published - 22 Jan 2008

Keywords

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

Access to Document

10.1016/j.entcs.2007.09.015

Cite this

@article{a45ade0ba1e646888f017ee795976df9,

title = "The λ-context Calculus",

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. {\textcopyright} 2008 Elsevier B.V. All rights reserved.",

keywords = "calculus of explicit substitutions, capture-avoiding substitution, capturing substitution, confluence, contexts, instantiation, Lambda-calculus, meta-variables, nominal techniques",

author = "Murdoch Gabbay and St{\'e}phane Lengrand",

year = "2008",

month = jan,

day = "22",

doi = "10.1016/j.entcs.2007.09.015",

language = "English",

volume = "196",

pages = "19--35",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "C",

}

TY - JOUR

T1 - The λ-context Calculus

AU - Gabbay, Murdoch

AU - Lengrand, Stéphane

PY - 2008/1/22

Y1 - 2008/1/22

N2 - 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.

AB - 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.

KW - calculus of explicit substitutions

KW - capture-avoiding substitution

KW - capturing substitution

KW - confluence

KW - contexts

KW - instantiation

KW - Lambda-calculus

KW - meta-variables

KW - nominal techniques

UR - https://www.scopus.com/pages/publications/38549133343

U2 - 10.1016/j.entcs.2007.09.015

DO - 10.1016/j.entcs.2007.09.015

M3 - Article

SN - 1571-0661

VL - 196

SP - 19

EP - 35

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - C

ER -

The λ-context Calculus

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this