Computing With Contexts A simple approach
David Sands · Electronic Notes in Theoretical Computer Science · 1998
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.