The reader learns how to use a proof assistant as a practical instrument for formal proofs concerning computer science artifacts as well as the art of exact logical reasoning from this book.

In this sense, it is a formal method of computer science, not merely semantics.

The book is appropriate for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic. The Isabelle formalization, including the proofs and accompanying slides, is freely available online.

The book is highly recommended for studying and teaching semantics and theorem proving while also learning much about higher-order logic.