Email Gateway (Aug 19 2022 at 14:03): Email Gateway (Aug 19 2022 at 14:03):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Apr 25 2024 at 16:19 UTC