author paulson
Tue, 05 Mar 1996 17:22:47 +0100
changeset 1544 ad47d58ecb37
parent 1543 53fe25620a03
child 1546 5d531aa23006
permissions -rw-r--r--
Corrected URL

<!-- $Id$ -->

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

Jacob Frost has mechanized the proofs from the article

  author	= "Robin Milner and Mads Tofte",
  title		= "Co-induction in Relational Semantics",
  journal	= TCS,
  year		= 1991,
  volume	= 87,
  pages		= "209--220"}

<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.

HREF="">report</A> describes this development.


<P>Last modified 5 March 1996