Lambda the Ultimate

"The paper is based upon categorical work on semantics, but explaining the ideas using Haskell makes them simpler, accessible to a wider audience, and executable."

This paper explains how to use fold and unfold to build executable semantic models. The equivalence between denotational semantics and folding over syntax trees is demonstrated with a simple example. A denotational semantics for addition is defined with fold and then redefined to compile "expressions into a list of instructions for execution using a stack." Next, the relation between unfold and operational semantics is illustrated:

"In operational semantics, the meaning of terms is defined using a transition relation that captures execution steps in an appropriate abstract machine... we explain how an operational semantics can be characterised as a semantics defined by unfolding to transition trees."

The last part of the paper deals with a more involved example: Milner's Calculus of Concurrent Systems (CCS) which is "defined in an abstract manner as least fixpoints of functors" again using Haskell. (Fold and Unfold for Program Semantics, Graham Hutton)