Concrete SemanticsThe 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 cor
