From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 04D5CBB81 for ; Thu, 9 Dec 2004 04:07:39 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iB937cpC002693 for ; Thu, 9 Dec 2004 04:07:38 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id EAA09117; Thu, 9 Dec 2004 04:07:38 +0100 (MET) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iB937Zd9015731; Thu, 9 Dec 2004 04:07:37 +0100 Received: from [192.168.1.200] (ppp203-65.lns1.syd3.internode.on.net [203.122.203.65]) by smtp3.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id iB937P7D075896; Thu, 9 Dec 2004 13:37:30 +1030 (CST) Subject: Re: [Caml-list] Type constraints From: skaller Reply-To: skaller@users.sourceforge.net To: Jacques Garrigue Cc: Alain.Frisch@inria.fr, caml-list In-Reply-To: <20041208.232322.07401394.garrigue@math.nagoya-u.ac.jp> References: <41B62407.4020102@inria.fr> <74A16EF6-4907-11D9-8195-000D9345235C@inria.fr> <41B6F610.8000507@inria.fr> <20041208.232322.07401394.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain Message-Id: <1102561644.2611.2.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 09 Dec 2004 14:07:24 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41B7C17A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41B7C178.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 coq:01 coq:01 glebe:01 061:98 assertions:01 nsw:01 typing:01 jacques:01 modules:01 constraints:01 snail:02 2037:02 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote: > Yet, modules are strange beasts for typing, so I wouldn't add the code > before thinking it through. I am curious as to the status of COQ support for verifying assertions about proposed changes to the type system. For example supposing you did 'think it through' and it seemed right, would you be able to then extend an existing COQ proof and attempt to prove your thinking mechanically? -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net