[PRL] structural operational semantics
Dave Herman
dherman at ccs.neu.edu
Tue May 23 14:25:20 EDT 2006
Can someone give me a hint as to what is meant by "structural
operational semantics?" I've been trying to infer it from this:
http://citeseer.ist.psu.edu/plotkin03origins.html
Plotkin seems to define it as an alternative to abstract machine
semantics. It doesn't seem to be specific to small-step or big-step, but
rather an operational semantics whose reduction rules are defined
inductively on the structure of terms?
In other words, it seems the obvious alternatives for defining an
operational semantics to work on entire programs are:
- extend the relation with the compatible closure
- define the relation via structural induction (SOS?)
- separate out the compatibility rules into a definition of evaluation
contexts & use Felleisen-style, context-sensitive reduction semantics
Is this accurate? Am I misunderstanding what is meant by SOS?
Thanks,
Dave
More information about the PRL
mailing list