[TYPES/announce] New Book: Concrete Semantics

[Tobias Nipkow]

                  Concrete Semantics -
               A Proof Assistant Approach
              Tobias Nipkow & Gerwin Klein

      http://www.in.tum.de/~nipkow/Concrete-Semantics/

We are pleased to announce the freely available electronic version
of this upcoming 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 correctness,
  (security) type systems, program analyses, denotational semantics,
  Hoare logic and abstract interpretation.

All of the material in Part II is formalized in Isabelle,
yet most of it can also be read independently of Part I.

The book has been classroom-tested extensively and contains
115 exercises that provide hands-on experience with Isabelle.
Slides and exercise templates are available online.

Enjoy!
Tobias & Gerwin