Abstract
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.
Users
Please
log in to take part in the discussion (add own reviews or comments).