src/ZF/Coind/README.html
author wenzelm
Wed, 21 May 1997 17:13:00 +0200
changeset 3279 815ef5848324
parent 1546 5d531aa23006
child 15283 f21466450330
permissions -rw-r--r--
tuned all READMEs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1543
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     1
<!-- $Id$ -->
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1546
diff changeset
     2
<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
1543
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
1544
ad47d58ecb37 Corrected URL
paulson
parents: 1543
diff changeset
    28
HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
1543
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    29
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1546
diff changeset
    30
</body>
815ef5848324 tuned all READMEs;
wenzelm
parents: 1546
diff changeset
    31
</html>