Concrete Semantics

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 Isabelle.
• 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 abstract interpretation.

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.

The files on this web site are compatible with Isabelle2022.

From a review on Amazon:

This is an excellent book. I found it made a great tutorial for theorem proving in Isabelle/HOL. I also found it a useful introduction to functional programming.

There are questions in the book with partially complete template answers available online. Profoundly difficult and frustrating at times but well worth the effort.

The book covers fundamental topics in computer science in the most rigorous way possible with elegant minimalist examples.