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.
No takes yet. Share an insight, caveat, or question.
Tobias Nipkow (1998) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: