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

Tobias Nipkow

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}}