Chapters 3 and 4 of the prog-prove document correspond to chapters 4
and 5 of “Concrete Semantics”.
(For the latter,
the PDF file included in the doc directory of the isabelle
distribution is currently the same as that on the
“Concrete Semantics” Website.)
Please use the “Concrete Semantics” numbering in your submission file
names, and document clearly if you internally use prog-prove numbering.
Note that the “Concrete Semantics” website also has an “Exercises” PDF document containing additional information and hints for the exercises in the “Concrete Semantics” book, accompanied by a package of template files.
(All the “Concrete Semantics” is mirrored in the “Concrete Semantics — local mirror” subsection on Avenue.)
Please send your Isabelle theories by e-mail to
kahl@cas.mcmaster.ca;
avoid splitting files more then necessary,
and avoid spaces and other
special characters in file names.
Work through chapter 3 of “Concrete Semantics”, including at least the exercises 3.1–3.5 and 3.7–3.8 — solving more is welcome!
Work through chapter 4 of “Concrete Semantics”, including at least the exercises 4.1–4.4 — solving more is welcome!
Please let me know whether, repectively how far,
you already have worked through “Concrete Semantics” chapter 5
(or prog-prove chapter 4).