Go backward to Denotations as Rewrite Rules Go up to Top Go forward to Computability of Phrases

Properties of Operational Semantics

• Soundness.
  • If p has an underlying "meaning" m and p => p', then p' means m as well.
  • By definition of =>.
• Subject reduction.
  • If p has an underlying "type" T and p => p', then p' has T as well.
  • By soundness of typing.
• Strong typing.
  • If p is well-typed and p => p', then p' contains no operator-operand incompatibilities.
  • By induction over computation rules.
• Computational adequacy.
  • A program p's underlying meaning is a proper meaning m, if there is some value v such that p => v and v means m.