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.