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 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id C1F31BC6B for ; Fri, 9 Nov 2007 13:20:22 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAIveM0eDbwiEnmdsb2JhbACPAQEBAQEHBAYp X-IronPort-AV: E=Sophos;i="4.21,394,1188770400"; d="scan'208";a="4064534" Received: from ppsw-2.csi.cam.ac.uk ([131.111.8.132]) by mail2-smtp-roc.national.inria.fr with ESMTP; 09 Nov 2007 13:20:22 +0100 X-Cam-SpamDetails: Not scanned X-Cam-AntiVirus: No virus found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from c160.al.cl.cam.ac.uk ([128.232.110.160]:50561) by ppsw-2.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.152]:587) with esmtpsa (PLAIN:so294) (TLSv1:AES128-SHA:128) id 1IqSqR-0005Ow-8g (Exim 4.63) for caml-list@yquem.inria.fr (return-path ); Fri, 09 Nov 2007 12:20:19 +0000 Mime-Version: 1.0 (Apple Message framework v752.2) Content-Transfer-Encoding: 7bit Message-Id: <2E0C2D8B-2512-4DEE-8F0C-21B29F4E912B@cl.cam.ac.uk> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: caml-list@yquem.inria.fr From: Scott Owens Subject: A sound semantics for OCaml light Date: Fri, 9 Nov 2007 12:20:19 +0000 X-Mailer: Apple Mail (2.752.2) Sender: Scott Owens X-Spam: no; 0.00; semantics:01 ocaml:01 ocaml:01 semantics:01 subset:01 coq:01 syntactic:01 theorem:02 caml:02 caml:02 objective:02 objective:02 algorithmic:02 executable:03 gilles:05 We are pleased to announce the public release of OCaml light, a formal semantics for a substantial, practical subset of the Objective Caml language. It is written in Ott, generating proof assistant definitions for HOL-4 and (in draft form) Coq and Isabelle/HOL. It comprises a small-step operational semantics and a syntactic, non- algorithmic type system. A type soundness theorem has been proved and mechanized using the HOL-4 proof assistant. To ensure that the operational semantics accurately models Objective Caml, an executable version of the semantics has been created (and proved equivalent in HOL to the original, relational version) and tested on a number of small test cases. For more information please visit http://www.cl.cam.ac.uk/~so294/ocaml. -Scott, Gilles, Peter, and Tom