The book Concrete Semantics
introduces semantics of programming
languages through the medium of a proof assistant. It consists of two parts:
Part I is a self-contained introduction to the proof assistant
Part II is an introduction to semantics and its applications and is based
on a simple imperative programming language. It covers the following topics:
operational semantics, compiler correctness, (security) type systems,
program analyses, denotational semantics, Hoare logic and
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.