Computing with Contexts: A simple approach. Sands, D. In Gordon, A. D., Pitts, A. M., & Talcott, C. L., editors, Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), volume 10, of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V., 1998.
Computing with Contexts: A simple approach [pdf]Paper  abstract   bibtex   
This article describes how the use of a higher-order syntax representation of contexts [due to A. Pitts] combines smoothly with higher-order syntax for evaluation rules, so that definitions can be extended to work over contexts. This provides "for free" - without the development of any new language-specific context calculi - evaluation rules for contexts which commute with hole-filling. We have found this to be a useful technique for directly reasoning about operational equivalence. A small illustration is given based on a unique fixed-point induction principle for a notion of guarded context in a functional language.

Downloads: 0