[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