src/ZF/Coind/README.html
author webertj
Mon, 07 Mar 2005 19:17:07 +0100
changeset 15582 7219facb3fd0
parent 15283 f21466450330
child 36862 952b2b102a0a
permissions -rw-r--r--
HTML 4.01 Transitional conformity

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<!-- $Id$ -->

<HTML>

<HEAD>
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <TITLE>ZF/Coind/README</TITLE>
</HEAD>

<BODY>

<H2>Coind -- A Coinduction Example</H2>

Jacob Frost has mechanized the proofs from the article

<P>
<PRE>
@Article{milner-coind,
  author	= "Robin Milner and Mads Tofte",
  title		= "Co-induction in Relational Semantics",
  journal	= TCS,
  year		= 1991,
  volume	= 87,
  pages		= "209--220"}
</PRE>

<P> It involves proving the consistency of the dynamic and static semantics
for a small functional language.  A codatatype definition specifies values and
value environments in mutual recursion: non-well-founded values represent
recursive functions; value environments are variant functions from variables
into values.

<P>
Frost's
<A
HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.

</body>
</html>