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

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

dvi
ps

At Springer: http://dx.doi.org/10.1007/s001650050009

BibTeX:

@article{Nipkow-FAC98,author={Tobias Nipkow},
title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
journal={Formal Aspects of Computing},volume=10,pages={171--186},year=1998}

The corresponding Isabelle theories.