Verification of Functional Code and Transition Systems
Rewriting techniques in the “A Computational Logic Handbook”
To determine: how to specify transition systems in expressive logic.
Mapping high-level data structures to sets, relations, and algebraic data types.