<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
<H2>IMP --- A <KBD>while</KBD>-Language and its 3 Semantics</H2>
The formalization of the denotational, operational and axiomatic semantics of
a simple while-language, including
<UL>
<LI> an equivalence proof between denotational and operational semantics and
<LI> the derivation of the Hoare rules from the denotational semantics.
</UL>
The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
<P>
<KBD>
@book{Winskel,author={Glynn Winskel},
title={The Formal Semantics of Programming Languages},
publisher={MIT Press},year=1993}
</KBD>
<P>
Here is the documentation.
</BODY></HTML>