src/ZF/IMP/README.html
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 15582 7219facb3fd0
child 36862 952b2b102a0a
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
paulson@1541
     3
<!-- $Id$ -->
webertj@15582
     4
webertj@15582
     5
<HTML>
webertj@15582
     6
webertj@15582
     7
<HEAD>
webertj@15582
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     9
  <TITLE>ZF/IMP/README</TITLE>
webertj@15582
    10
</HEAD>
webertj@15582
    11
webertj@15582
    12
<BODY>
nipkow@1522
    13
paulson@1541
    14
<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
nipkow@1522
    15
webertj@15283
    16
The formalization of the denotational and operational semantics of a simple
webertj@15283
    17
while-language together with an equivalence proof between the two semantics.
webertj@15283
    18
The whole development essentially formalizes/transcribes chapters 2 and 5 of
nipkow@1522
    19
<P>
nipkow@1522
    20
<PRE>
nipkow@1522
    21
@book{Winskel,
nipkow@1522
    22
 author = {Glynn Winskel},
nipkow@1522
    23
 title = {The Formal Semantics of Programming Languages},
nipkow@1522
    24
 publisher = {MIT Press},
nipkow@1522
    25
 year = 1993}.
nipkow@1522
    26
</PRE>
nipkow@1522
    27
<P>
webertj@15283
    28
There is a
webertj@15283
    29
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A>
webertj@15283
    30
by L&ouml;tzbeyer and Sandner.
nipkow@1522
    31
<P>
nipkow@1522
    32
A much extended version of this development is found in
paulson@1541
    33
<A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
nipkow@1522
    34
</BODY></HTML>