• The book shows that a semantics is not a collection of abstract symbols on sheets of paper but formal text that can be checked and executed by the computer: Isabelle is also a programming environment and most of the definitions in the book are executable and can even be exported as programs in a number of (functional) programming languages. For a computer scientist, this is as concrete as it gets.
• Much of the book deals with concrete applications of semantics: compilers, type systems, program analysers.
• The predominant formalism in the book is operational semantics, the most concrete of the various forms of semantics.
