src/HOL/IMP/README.html
author paulson
Wed May 07 13:50:52 1997 +0200 (1997-05-07)
changeset 3124 1c0dfa7ebb72
parent 2796 c23e367e57be
permissions -rw-r--r--
changed title to README
     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>