Implicit Propagation in Structural Operational Semantics

Peter D Mosses (joint work with Mark New)


In contrast to a transition system specification in process algebra,
a structural operational semantics (SOS) of a programming language
usually involves auxiliary entities: stores, environments, etc.
When specifying SOS rules, particular auxiliary entities often
need to be propagated unchanged between premises and conclusions.
The standard technique is to make such propagation explicit, using
variables. However, referring to all entities that need to be
propagated unchanged in each rule can be tedious, and it hinders
direct reuse of rules in different language descriptions.

This talk proposes a new interpretation of SOS rules, such that
each auxiliary entity is implicitly propagated in all rules in
which it is not mentioned. The main benefits include significant
notational simplification of SOS rules and much-improved reusability.
This new interpretation of SOS rules is based on the same
foundations as Modular SOS, but avoids the notational overhead
of grouping auxiliary entities together in labels.

After motivating and explaining implicit propagation, we recall
the foundations of SOS and Modular SOS specifications, and define
the meaning of SOS specifications with implicit propagation by
translating them to Modular SOS. We then show how implicit
propagation can simplify various rules found in the SOS literature.
Finally, we propose the use of the new framework in connection
with so-called 'constructive semantics'.


The talk is based on a paper that has been accepted for the
SOS workshop at ICALP this summer. Copies will be handed out
at the seminar.

Tuesday 20th May 2008, 14:00
Robert Recorde Room
Department of Computer Science