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.