A new calculus of contexts

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.1 Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: lambda calculus and related systems General Terms: Theory.

• Type: Conference
• Year: 2005
• Where: PPDP
• Authors: Murdoch Gabbay
• Keywords: Applicative Characterisation, Hindley-Milner Type System, PPDP 2005, Systems General Terms