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
nipkow@1340
     1
<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
nipkow@1340
     2
nipkow@1696
     3
<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
nipkow@1340
     4
nipkow@1696
     5
The denotational, operational, and axiomatic semantics, a verification
nipkow@1696
     6
condition generator, and all the necessary soundness, completeness and
nipkow@1696
     7
equivalence proofs. Essentially a formalization of the first 100 pages
nipkow@1696
     8
of
nipkow@1696
     9
<PRE>
nipkow@1447
    10
@book{Winskel, author = {Glynn Winskel},
nipkow@1447
    11
title = {The Formal Semantics of Programming Languages},
nipkow@1447
    12
publisher = {MIT Press}, year = 1993}
nipkow@1696
    13
</PRE>
nipkow@1340
    14
<P>
nipkow@1696
    15
An eminently readable description of this theory is found
nipkow@1923
    16
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html">
nipkow@1696
    17
here</A>.
nipkow@2796
    18
<P>
nipkow@2796
    19
A denotational semantics for IMP based on HOLCF is found
nipkow@2796
    20
<A HREF="../../HOLCF/IMP/index.html">here</A>.
nipkow@1340
    21
</BODY></HTML>