src/ZF/Coind/README.html
author paulson
Tue, 05 Mar 1996 16:50:17 +0100
changeset 1543 53fe25620a03
child 1544 ad47d58ecb37
permissions -rw-r--r--
New documentation for examples
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1543
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     1
<!-- $Id$ -->
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     2
<HTML><HEAD><TITLE>HOL/Coind</TITLE></HEAD><BODY>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     3
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     4
<H2>Coind -- A Coinduction Example</H2>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     5
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     6
Jacob Frost has mechanized the proofs from the article
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     7
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     8
<P>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     9
<PRE>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    10
@Article{milner-coind,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    11
  author	= "Robin Milner and Mads Tofte",
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    12
  title		= "Co-induction in Relational Semantics",
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    13
  journal	= TCS,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    14
  year		= 1991,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    15
  volume	= 87,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    16
  pages		= "209--220"}
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    17
</PRE>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    18
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    19
<P> It involves proving the consistency of the dynamic and static semantics
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    20
for a small functional language.  A codatatype definition specifies values and
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    21
value environments in mutual recursion: non-well-founded values represent
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    22
recursive functions; value environments are variant functions from variables
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    23
into values.
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    24
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    25
<P>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    26
Frost's
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    27
<A
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    28
HREF="http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    29
<P>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    30
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    31
<HR>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    32
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    33
<P>Last modified 5 March 1996