src/ZF/Coind/README.html
author paulson
Tue, 05 Mar 1996 17:29:58 +0100
changeset 1546 5d531aa23006
parent 1544 ad47d58ecb37
child 3279 815ef5848324
permissions -rw-r--r--
Changed HOL to ZF in title; added address
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1543
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
     1
<!-- $Id$ -->
1546
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
     2
<HTML><HEAD><TITLE>ZF/Coind</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
<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
1546
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
    34
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
    35
<ADDRESS>
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
    36
<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
    37
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
5d531aa23006 Changed HOL to ZF in title; added address
paulson
parents: 1544
diff changeset
    38
</ADDRESS>