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