From: Alfio Martini <alfio.martini@acm.org>
Dear Tobias and Gerwin,
First of all, thank you both for the excellent book on Concrete Semantics.
It is very polished
and contains a wealth of material that is nowhere to be found in a single
book.
Besides, its innovative, concrete approach with the Isabelle proof
assistant
will certainly increase the interest of many computing professionals and
students alike for the study of semantics of programming languages.
However, in the page
http://www21.in.tum.de/~nipkow/semantics/,
the IMP theories (either as .thy files or as a PDF document) are not
available (broken link). Can I assume that they are the ones that
are distributed with Isabelle?
Best!
From: Tobias Nipkow <nipkow@in.tum.de>
Dear Alfio,
The IMP theories are indeed the ones in the distribution, but you need
Isabelle2013-1 for that, not Isabelle2013.
Thank you for your kind words.
Tobias
From: Gergely Buday <gbuday@gmail.com>
Dear Mr. Nipkow,
from the hg id I guess that this is under development. Will there be a
release for the book?
From: Tobias Nipkow <nipkow@in.tum.de>
The main text is practically finished, we are currently working on the exercises
only - we add them incrementally. At some point we do intend to announce a release.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC