From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 5F113BC0B for ; Fri, 2 Feb 2007 15:09:22 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l12E9LUO031948 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 2 Feb 2007 15:09:22 +0100 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 7E9E3202139; Fri, 2 Feb 2007 15:09:21 +0100 (CET) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id 16A1FCED98; Fri, 2 Feb 2007 15:09:21 +0100 (CET) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1HCz6P-0003Es-00; Fri, 02 Feb 2007 15:09:21 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <17859.17937.213238.86493@serveur9-10.lri.fr> Date: Fri, 2 Feb 2007 15:09:21 +0100 From: Jean-Christophe Filliatre To: oleg@pobox.com Cc: caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si Subject: Re: [Caml-list] Programming with correctness guarantees In-Reply-To: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> X-Mailer: VM 7.19 under Emacs 21.4.1 X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at discorde with ID 45C34611.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 tackled:01 ocaml:01 caml-list:01 algorithm:01 theorem:02 programming:03 programming:03 languages:03 thread:05 provers:05 ridge:92 correctness:08 > > it would be interesting to augment real programming > > languages with ways of writing specifications that can then be tackled > > by theorem provers and proof asistants. Some readers of this thread may be interested by the following proof of an OCaml implementation of Peterson's algorithm by Tom Ridge: http://www.cl.cam.ac.uk/~tjr22/doc/concTalk20070124.pdf -- Jean-Christophe