Concrete Semantics

Tutorial for Isabelle/HOL, and formally specifying a toy language.

http://concrete-semantics.org/
concrete-semantics.pdf (1.6 MB)