How are various language constructs made concrete?
Syntax
Use BNF style.
EXP ::= ...
| Exp = Exp [strict(2)]
Configurations
Snapshot of project execution.
- Remaining program
- 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.