IMP --- A WHILE-language and its Semantics

The denotational, operational, and axiomatic semantics, a verification condition generator, and all the necessary soundness, completeness and equivalence proofs. Essentially a formalization of the first 100 pages of
@book{Winskel, author = {Glynn Winskel},
title = {The Formal Semantics of Programming Languages},
publisher = {MIT Press}, year = 1993}

An eminently readable description of this theory is found here.

A denotational semantics for IMP based on HOLCF is found here.