Index of /ports/math/isabelle/work/Isabelle/src/ZF/Coind

 Name                    Last modified       Size  Description

 Parent Directory        09-Aug-2008 06:10      -  
 Dynamic.thy             17-Jun-2005 07:15     2k  
 Dynamic.thy.html        09-Aug-2008 06:10     0k  
 ECR.thy                 17-Jun-2005 07:15     6k  
 ECR.thy.html            09-Aug-2008 06:10     0k  
 Language.thy            17-Jun-2005 07:15     1k  
 Language.thy.html       09-Aug-2008 06:10     0k  
 Map.thy                 17-Jun-2005 07:15     5k  
 Map.thy.html            09-Aug-2008 06:10     0k  
 ROOT.ML                 25-Dec-2001 01:02     1k  
 ROOT.ML.html            09-Aug-2008 06:10     0k  
 Static.thy              17-Jun-2005 07:15     2k  
 Static.thy.html         09-Aug-2008 06:10     0k  
 Types.thy               17-Jun-2005 07:15     2k  
 Types.thy.html          09-Aug-2008 06:10     0k  
 Values.thy              17-Jun-2005 07:15     3k  
 Values.thy.html         09-Aug-2008 06:10     0k  

Coind -- A Coinduction Example

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

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.

Frost's report describes this development.