src/ZF/Coind/README.html
author wenzelm
Wed, 12 May 2010 14:17:26 +0200
changeset 36862 952b2b102a0a
parent 15582 7219facb3fd0
permissions -rw-r--r--
removed obsolete CVS Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 3279
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 3279
diff changeset
     2
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     3
<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
  <TITLE>ZF/Coind/README</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
<BODY>
1543
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    11
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    12
<H2>Coind -- A Coinduction Example</H2>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    13
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    14
Jacob Frost has mechanized the proofs from the article
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    15
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    16
<P>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    17
<PRE>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    18
@Article{milner-coind,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    19
  author	= "Robin Milner and Mads Tofte",
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    20
  title		= "Co-induction in Relational Semantics",
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    21
  journal	= TCS,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    22
  year		= 1991,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    23
  volume	= 87,
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    24
  pages		= "209--220"}
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    25
</PRE>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    26
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    27
<P> It involves proving the consistency of the dynamic and static semantics
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    28
for a small functional language.  A codatatype definition specifies values and
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    29
value environments in mutual recursion: non-well-founded values represent
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    30
recursive functions; value environments are variant functions from variables
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    31
into values.
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    32
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    33
<P>
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    34
Frost's
53fe25620a03 New documentation for examples
paulson
parents:
diff changeset
    35
<A
1544
ad47d58ecb37 Corrected URL
paulson
parents: 1543
diff changeset
    36
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
    37
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1546
diff changeset
    38
</body>
815ef5848324 tuned all READMEs;
wenzelm
parents: 1546
diff changeset
    39
</html>