Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 SOS'04 invited tutorial, David Sands
Representing and Manipulating Contexts A Tool for Operational Reasoning
David Sands
Invited tutorial at SOS'04,
Structural Operational Semantics Workshop,
August 30, 2004
London, England
Abstract
The notion of a context is widely used in programming language
semantics -- for example in the definition of operational
equivalences, or program transformation, and in certain styles of
operational semantics definitions. This tutorial describes how the use
of a higher-order syntax representation of contexts 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. Some illustrations of the utility of this
technique will be given.