From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id CCD5BBBBB for ; Sun, 22 Jan 2006 18:27:30 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0MHRUBw025603 for ; Sun, 22 Jan 2006 18:27:30 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA32718 for ; Sun, 22 Jan 2006 18:27:29 +0100 (MET) Received: from ns3.frap.net (ns3.frap.net [69.93.35.202]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k0MHRS7V027704 for ; Sun, 22 Jan 2006 18:27:29 +0100 Received: from localhost (fsh-cpe-52-173.resnet.ucsc.edu [169.233.52.173]) by ns3.frap.net (Postfix) with ESMTP id 7E60556AE88; Sun, 22 Jan 2006 09:27:29 -0800 (PST) Date: Sun, 22 Jan 2006 09:26:34 -0800 From: Kenn Knowles To: Andrej Bauer Cc: Caml list Subject: Re: [Caml-list] Coinductive semantics Message-ID: <20060122172634.GA6353@tallman.kefka.frap.net> References: <1137163342.3681.533.camel@rosella> <1137594157.8943.106.camel@rosella> <20060120004948.GA2490@coruscant.stwing.upenn.edu> <43D0B413.1060806@andrej.com> <20060120185911.GA22920@coruscant.stwing.upenn.edu> <1137790790.15137.39.camel@rosella> <43D27F18.9030102@andrej.com> <1137899816.885.45.camel@rosella> <43D37955.90408@andrej.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <43D37955.90408@andrej.com> User-Agent: Mutt/1.5.11 X-Miltered: at concorde with ID 43D3C082.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 43D3C080.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 coinductive:01 semantics:01 andrej:01 compiler:01 knowles:98 wrote:01 dependent:02 bottom:93 edu:07 edu:07 cases:08 bauer:09 might:10 sort:11 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 On Sun, Jan 22, 2006 at 01:23:49PM +0100, Andrej Bauer wrote: > There may be special cases where compiler can determine whether the > index is ok. > [...] > I am sure > people have looked into this sort of thing. Good luck! Yes. One might be interested in Dependent ML, or the references at the bottom of the page. http://www.cs.bu.edu/~hwxi/DML/DML.html - Kenn