Winskel is (almost) right: Towards a mechanized semantics textbook

Related Items

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs, Executable structural operational semantics in Maude, Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm, Some Domain Theory and Denotational Semantics in Coq, Introduction to ``Milestones in interactive theorem proving, Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, Second-order properties of undirected graphs, Relation-algebraic verification of Borůvka's minimum spanning tree algorithm, Relational characterisations of paths, On theorem prover-based testing, Verifying minimum spanning tree algorithms with Stone relation algebras, All-Path Reachability Logic, A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL, Proving pointer programs in higher-order logic, An algebraic framework for minimum spanning tree problems, Matching Logic: An Alternative to Hoare/Floyd Logic, Building program construction and verification tools from algebraic principles, An extensible encoding of object-oriented data models in HOL. With an application to IMP++

Uses Software