The book Concrete Semantics
introduces semantics of programming
languages through the medium of a proof assistant. The first part of the book
is an introduction to the proof assistant Isabelle
. The second part 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. The book contains over 120 exercises.