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