[PRL] structural operational semantics

[Dave Herman]

> Wait, I thought some of Plotkin's rules have antecedents, 
> meaning it's not entirely small-step.

Are you being silly, or are you aware that that's a false dichotomy? 
Gentzen-style inference rules are one way to set up the compatible 
closure rules on a small-step semantics.

Felleisen:

     E ::= [] | (E e) | (v E)
     E[(\x.M v)] -> E[M[v/x]]

Plotkin? Barendregt? The mind of God?

     ------------------
     (\x.M v) -> M[v/x]

         M -> M'
     ---------------
     (M N) -> (M' N)

         M -> M'
     ---------------
     (v M) -> (v M')

That's still small-step.

Dave