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