Winskel is (almost) Right

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

Tobias Nipkow

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.

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.