#### Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

We present a formalization of the first 100 pages of Winskel's `The Formal
Semantics of Programming Languages' in the theorem prover Isabelle/HOL: 2
operational, 2 denotational, 1 axiomatic semantics, a verification condition
generator, and the necessary soundness, completeness and equivalence proofs,
all for a simple imperative language.
**Note**:
There is an extended journal version.

dvi
ps

BibTeX:

@inproceedings{Nipkow-FSTTCS-96,author={Tobias Nipkow},
title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
booktitle=
{Foundations of Software Technology and Theoretical Computer Science},
editor={V. Chandru and V. Vinay},
publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192},
url={http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.dvi.gz}}