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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 85674BBC1 for ; Wed, 13 Feb 2008 11:19:59 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKZSskeA6AAOn2dsb2JhbACQPAEBAQEBBgQGCQgYnEc X-IronPort-AV: E=Sophos;i="4.25,345,1199660400"; d="scan'208";a="8016351" Received: from mta2.cl.cam.ac.uk ([128.232.0.14]) by mail1-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 11:19:59 +0100 Received: from optic.cl.cam.ac.uk ([128.232.9.31] helo=cl.cam.ac.uk) by mta2.cl.cam.ac.uk with esmtp (Exim 3.092 #1) id 1JPEic-0004I9-00; Wed, 13 Feb 2008 10:19:58 +0000 To: caml-list@yquem.inria.fr Cc: Peter.Sewell@cl.cam.ac.uk Subject: Re: Caml-list Digest, Vol 32, Issue 43 In-reply-to: <20080213100127.24366BC73@yquem.inria.fr> References: <20080213100127.24366BC73@yquem.inria.fr> Comments: In-reply-to caml-list-request@yquem.inria.fr message dated "Wed, 13 Feb 2008 11:01:27 +0100." Date: Wed, 13 Feb 2008 10:19:58 +0000 From: Peter Sewell Message-Id: X-Spam: no; 0.00; andrej:01 andrej:01 ocaml:01 compiler:01 ocaml:01 formalized:01 compiler:01 formalized:01 variants:01 xavier's:01 semantics:01 wrote:01 wrote:01 typing:01 caml-list:01 Jacques Garrigue wrote: >Andrej Bauer wrote: >> Out of curiosity, is there a document describing the current ocaml >> typing system, other than the compiler source code? >> >> More generally, what level of formal specification and verification does >> ocaml reach? None, well commented code, a fragment of the language is >> formalized, someone's PhD described the compiler, there is an official >> document describing the compiler, God gave Xavier the type system on Mt >> Blanc, or what? > >Most of the type system is formalized, but there is no single place to >look at. Caml Special Light (ocaml minus objects and variants) was >mostly based on Xavier's work, so you can look at at his papers for that part Also for that part of the language, Scott Owens has a type system and operational semantics, with a formalised soundness proof: http://www.cl.cam.ac.uk/~so294/ocaml/ It's not a normative specification, but does aim to be rather close to the behaviour of the implementation. Peter