Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

Tobias Nipkow

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.

Note: There is an extended journal version.

dvi ps


@inproceedings{Nipkow-FSTTCS-96,author={Tobias Nipkow},
title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
{Foundations of Software Technology and Theoretical Computer Science},
editor={V. Chandru and V. Vinay},