The context calculus lambda-c

Mirna Bognar and Roel de Vrijer

  The calculus lambda-c serves as a general framework for representing 
  contexts. Essential features are control over variable capturing and 
  the freedom to manipulate contexts before or after hole filling, by 
  a mechanism of delayed substitution.
  The context calculus lambda-c is given in the form of an extension of 
  the lambda calculus. 
  Many notions of context can be represented within the framework;
  a particular variation can be obtained by the choice of a so-called 
  pretyping. By way of an example we treat the contexts of Hashimoto & Ohori.