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