src/HOL/IMP/README.html
changeset 3124 1c0dfa7ebb72
parent 2796 c23e367e57be
equal deleted inserted replaced
3123:f58719b49cae 3124:1c0dfa7ebb72
     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>