equal
deleted
inserted
replaced
1 <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY> |
1 <!-- $Id$ --> |
|
2 <HTML><HEAD><TITLE>HOL/IMP</TITLE></HEAD><BODY> |
2 |
3 |
3 <H2>IMP --- A <KBD>while</KBD>-language and two semantics</H2> |
4 <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2> |
4 |
5 |
5 The formalization of the denotational and operational semantics of |
6 The formalization of the denotational and operational semantics of |
6 a simple while-language together with an equivalence proof between the two |
7 a simple while-language together with an equivalence proof between the two |
7 semantics. The whole development essentially formalizes/transcribes chapters |
8 semantics. The whole development essentially formalizes/transcribes chapters |
8 2 and 5 of |
9 2 and 5 of |
13 title = {The Formal Semantics of Programming Languages}, |
14 title = {The Formal Semantics of Programming Languages}, |
14 publisher = {MIT Press}, |
15 publisher = {MIT Press}, |
15 year = 1993}. |
16 year = 1993}. |
16 </PRE> |
17 </PRE> |
17 <P> |
18 <P> |
18 Some documentation is found |
19 There is a |
19 <A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz> |
20 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz"> |
20 here</A> |
21 report</A> by Lötzbeyer and Sandner. |
21 <P> |
22 <P> |
22 A much extended version of this development is found in |
23 A much extended version of this development is found in |
23 <A HREF=../../HOL/IMP/index.html>HOL/IMP</A>. |
24 <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>. |
24 </BODY></HTML> |
25 </BODY></HTML> |
|
26 |
|
27 <HR> |
|
28 |
|
29 <P>Last modified 5 March 1996 |