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 operational semantics and its applications and is based on a
simple imperative programming language.