## IMP -- A `while`-language and two semantics

The formalization of the denotational and operational semantics of a simple while-language together with an equivalence proof between the two semantics. The whole development essentially formalizes/transcribes chapters 2 and 5 of

    @book{Winskel,
     author = {Glynn Winskel},
     title = {The Formal Semantics of Programming Languages},
     publisher = {MIT Press},
     year = 1993}.

There is a report by Lötzbeyer and Sandner.

A much extended version of this development is found in HOL/IMP.