A new calculus of contexts
Murdoch J. Gabbay · 2005
We study contexts (terms with holes) by proposing a 'λ-calculus with holes'. It is very expressive and can encode programming constructs apparently unrelated to contexts, including objects and algorithms in partial evaluation. We give proofs of confluence, preservation of strong normalisation, principal typing for an ML-style Hindley-Milner type system, and an applicative characterisation of contextual equivalence. We explore the limitations of the calculus including further applications, and discuss how they might be tackled.