How are various language constructs made concrete?


Use BNF style.

EXP ::= ...
      | Exp = Exp [strict(2)]


Snapshot of project execution.

  1. Remaining program
  2. Execution State e.g. registers, mem, stack, PC, rand, in, out, env, etc…

Structured as a nested cell structure (similar to XML). Leaves can be sets, multisets, lists, maps, etc…

Allows you to traverse semantics as state changes.