src/HOL/IMP/README.html
author paulson
Wed, 07 May 1997 13:50:52 +0200
changeset 3124 1c0dfa7ebb72
parent 2796 c23e367e57be
permissions -rw-r--r--
changed title to README
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3124
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
     1
<!-- $Id$ -->
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
     2
<HTML><HEAD><TITLE>HOL/IMP/README</TITLE></HEAD><BODY>
1340
71b0a5d83347 *** empty log message ***
nipkow
parents:
diff changeset
     3
3124
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
     4
<H2>IMP--A <KBD>WHILE</KBD>-language and its Semantics</H2>
1340
71b0a5d83347 *** empty log message ***
nipkow
parents:
diff changeset
     5
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
     6
The denotational, operational, and axiomatic semantics, a verification
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
     7
condition generator, and all the necessary soundness, completeness and
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
     8
equivalence proofs. Essentially a formalization of the first 100 pages
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
     9
of
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
    10
<PRE>
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1340
diff changeset
    11
@book{Winskel, author = {Glynn Winskel},
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1340
diff changeset
    12
title = {The Formal Semantics of Programming Languages},
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1340
diff changeset
    13
publisher = {MIT Press}, year = 1993}
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
    14
</PRE>
1340
71b0a5d83347 *** empty log message ***
nipkow
parents:
diff changeset
    15
<P>
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
    16
An eminently readable description of this theory is found
1923
e100f28ffc18 updated html-link
nipkow
parents: 1696
diff changeset
    17
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html">
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1447
diff changeset
    18
here</A>.
2796
c23e367e57be Added link to HOLCF/IMP
nipkow
parents: 1923
diff changeset
    19
<P>
c23e367e57be Added link to HOLCF/IMP
nipkow
parents: 1923
diff changeset
    20
A denotational semantics for IMP based on HOLCF is found
c23e367e57be Added link to HOLCF/IMP
nipkow
parents: 1923
diff changeset
    21
<A HREF="../../HOLCF/IMP/index.html">here</A>.
3124
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
    22
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
    23
<HR>
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
    24
<P>Last modified 7 May 1997
1c0dfa7ebb72 changed title to README
paulson
parents: 2796
diff changeset
    25
1340
71b0a5d83347 *** empty log message ***
nipkow
parents:
diff changeset
    26
</BODY></HTML>