Winskel is (almost) Right: Towards a Mechanized Semantics Textbook
Tobias Nipkow · Formal Aspects of Computing · 1998
Abstract. 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.