Concrete Semantics

Concrete Semantics

with Isabelle/HOL

Tobias Nipkow and Gerwin Klein

The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. It consists of two parts: All of the material in Part II is formalized in Isabelle, yet most of it can also be read independently of Part I.

The book contains 115 exercises that provide hands-on experience with Isabelle. Templates are available here.

The book has been classroom-tested extensively. Slides are available here.