src/HOL/IMP/README.html
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 3124 1c0dfa7ebb72
permissions -rw-r--r--
Basis now Main.
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/IMP/README</TITLE></HEAD><BODY>
     3 
     4 <H2>IMP--A <KBD>WHILE</KBD>-language and its Semantics</H2>
     5 
     6 The denotational, operational, and axiomatic semantics, a verification
     7 condition generator, and all the necessary soundness, completeness and
     8 equivalence proofs. Essentially a formalization of the first 100 pages
     9 of
    10 <PRE>
    11 @book{Winskel, author = {Glynn Winskel},
    12 title = {The Formal Semantics of Programming Languages},
    13 publisher = {MIT Press}, year = 1993}
    14 </PRE>
    15 <P>
    16 An eminently readable description of this theory is found
    17 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html">
    18 here</A>.
    19 <P>
    20 A denotational semantics for IMP based on HOLCF is found
    21 <A HREF="../../HOLCF/IMP/index.html">here</A>.
    22 
    23 <HR>
    24 <P>Last modified 7 May 1997
    25 
    26 </BODY></HTML>