Higher-Order and Symbolic Computation, 12(2)171-201

Computing with Contexts

Ian A. Mason, School of Mathematical and Computer Sciences, University of New England, NSW, Australia, 2351

Abstract: We investigate a representation of contexts, expressions with holes in them, that enables them to be meaningfully transformed, in particular alpha-converted and beta-reduced. In particular we generalize the set of lambda-expressions to include holes, and on these generalized entities define beta-reduction (i.e., substitution) and filling so that these operations preserve alpha-congruence and commute. The theory is then applied to allow the encoding of reduction systems and operational semantics of call-by-value calculi enriched with control, imperative and concurrent features.

Keywords: lambda-calculus, contexts, operational semantics, theorem proving

This article can be downloaded [here]. 		[picture of journal cover]

June 2003 - hosc@brics.dk