src/ZF/Coind/README.html
changeset 1543 53fe25620a03
child 1544 ad47d58ecb37
equal deleted inserted replaced
1542:03e727af711d 1543:53fe25620a03
       
     1 <!-- $Id$ -->
       
     2 <HTML><HEAD><TITLE>HOL/Coind</TITLE></HEAD><BODY>
       
     3 
       
     4 <H2>Coind -- A Coinduction Example</H2>
       
     5 
       
     6 Jacob Frost has mechanized the proofs from the article
       
     7 
       
     8 <P>
       
     9 <PRE>
       
    10 @Article{milner-coind,
       
    11   author	= "Robin Milner and Mads Tofte",
       
    12   title		= "Co-induction in Relational Semantics",
       
    13   journal	= TCS,
       
    14   year		= 1991,
       
    15   volume	= 87,
       
    16   pages		= "209--220"}
       
    17 </PRE>
       
    18 
       
    19 <P> It involves proving the consistency of the dynamic and static semantics
       
    20 for a small functional language.  A codatatype definition specifies values and
       
    21 value environments in mutual recursion: non-well-founded values represent
       
    22 recursive functions; value environments are variant functions from variables
       
    23 into values.
       
    24 
       
    25 <P>
       
    26 Frost's
       
    27 <A
       
    28 HREF="http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
       
    29 <P>
       
    30 
       
    31 <HR>
       
    32 
       
    33 <P>Last modified 5 March 1996