We present a formalization of the first 100 pages of Winskel's The Formal Semantics of Programming Languages in the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 1 axiomatic semantics, a verification condition generator, and the necessary soundness, completeness and equivalence proofs, all for a simple imperative language.
CITATION STYLE
Nipkow, T. (1996). Winskel is (almost) right: Towards a mechanized semantics textbook. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1180, pp. 180–192). Springer Verlag. https://doi.org/10.1007/3-540-62034-6_48
Mendeley helps you to discover research relevant for your work.