src/HOL/IMP/README.html
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2796 c23e367e57be
child 3124 1c0dfa7ebb72
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
     2 
     3 <H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
     4 
     5 The denotational, operational, and axiomatic semantics, a verification
     6 condition generator, and all the necessary soundness, completeness and
     7 equivalence proofs. Essentially a formalization of the first 100 pages
     8 of
     9 <PRE>
    10 @book{Winskel, author = {Glynn Winskel},
    11 title = {The Formal Semantics of Programming Languages},
    12 publisher = {MIT Press}, year = 1993}
    13 </PRE>
    14 <P>
    15 An eminently readable description of this theory is found
    16 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html">
    17 here</A>.
    18 <P>
    19 A denotational semantics for IMP based on HOLCF is found
    20 <A HREF="../../HOLCF/IMP/index.html">here</A>.
    21 </BODY></HTML>