A new calculus of contexts

9 years 4 months ago
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.
Murdoch Gabbay
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where PPDP
Authors Murdoch Gabbay
Comments (0)