equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY> |
1 <!-- $Id$ --> |
|
2 <HTML><HEAD><TITLE>HOL/IMP/README</TITLE></HEAD><BODY> |
2 |
3 |
3 <H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2> |
4 <H2>IMP--A <KBD>WHILE</KBD>-language and its Semantics</H2> |
4 |
5 |
5 The denotational, operational, and axiomatic semantics, a verification |
6 The denotational, operational, and axiomatic semantics, a verification |
6 condition generator, and all the necessary soundness, completeness and |
7 condition generator, and all the necessary soundness, completeness and |
7 equivalence proofs. Essentially a formalization of the first 100 pages |
8 equivalence proofs. Essentially a formalization of the first 100 pages |
8 of |
9 of |
16 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html"> |
17 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html"> |
17 here</A>. |
18 here</A>. |
18 <P> |
19 <P> |
19 A denotational semantics for IMP based on HOLCF is found |
20 A denotational semantics for IMP based on HOLCF is found |
20 <A HREF="../../HOLCF/IMP/index.html">here</A>. |
21 <A HREF="../../HOLCF/IMP/index.html">here</A>. |
|
22 |
|
23 <HR> |
|
24 <P>Last modified 7 May 1997 |
|
25 |
21 </BODY></HTML> |
26 </BODY></HTML> |