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. 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.