| The context calculus λc (Extended Abstract) (1999) | |||||||||||||||
Abstract | |||||||||||||||
| Mirna Bognar Roel de Vrijer Abstract The calculus 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 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. 1 Introduction The central notion in this paper is that of context, i.e. an expression with special places, called holes, where other expressions can be placed. For example, in the lambda calculus, (x:2)z, where 2 denotes a hole, is a context. In formal systems with bound variables, such as -calculus, a distinctive feature of placing an arbitrary expression into a hole of a context is variable capturing: some free varia... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||