[racket] Inductive and coinductive reasoning? (was "shared and immutable structures")

On Wed, Feb 02, 2011 at 04:39:07PM -0800, mike at goblin.punk.net wrote:
> On Wed, Feb 02, 2011 at 11:30:45AM -0500, Shriram Krishnamurthi wrote:
> > Yes you do.  Far less useful at our level.  But shared + immutable
> > gives you coinductive.  That's why the distinction helps.
> 
> I'm not familiar with these terms and had trouble follwiong that
> thread.  Would someone explain or point me to appropriate reading?

I found a more comprehensible reference:

http://tunes.org/wiki/induction_20and_20co-induction.html

This is from the tunes project.  It's an interesting project in which 
ntends to use formal proof techniques to provide security.  I say 
"intends" because the last time I looked seriously through their web 
sites, they seemed to be interminably stuck in planning more.

-- hendrik