|
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
1 <!-- $Id$ --> |
3 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY> |
4 <HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY> |
3 |
5 |
4 <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2> |
6 <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2> |
5 |
7 |
6 The formalization of the denotational and operational semantics of |
8 The formalization of the denotational and operational semantics of a simple |
7 a simple while-language together with an equivalence proof between the two |
9 while-language together with an equivalence proof between the two semantics. |
8 semantics. The whole development essentially formalizes/transcribes chapters |
10 The whole development essentially formalizes/transcribes chapters 2 and 5 of |
9 2 and 5 of |
|
10 <P> |
11 <P> |
11 <PRE> |
12 <PRE> |
12 @book{Winskel, |
13 @book{Winskel, |
13 author = {Glynn Winskel}, |
14 author = {Glynn Winskel}, |
14 title = {The Formal Semantics of Programming Languages}, |
15 title = {The Formal Semantics of Programming Languages}, |
15 publisher = {MIT Press}, |
16 publisher = {MIT Press}, |
16 year = 1993}. |
17 year = 1993}. |
17 </PRE> |
18 </PRE> |
18 <P> |
19 <P> |
19 There is a |
20 There is a |
20 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz"> |
21 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A> |
21 report</A> by Lötzbeyer and Sandner. |
22 by Lötzbeyer and Sandner. |
22 <P> |
23 <P> |
23 A much extended version of this development is found in |
24 A much extended version of this development is found in |
24 <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>. |
25 <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>. |
25 </BODY></HTML> |
26 </BODY></HTML> |