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=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr 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 490EBBC6D for ; Tue, 12 Feb 2008 11:35:21 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAKoEsUfAXQImh2dsb2JhbACQOwEBAQgKKZsH X-IronPort-AV: E=Sophos;i="4.25,339,1199660400"; d="scan'208";a="7218172" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Feb 2008 11:35:21 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m1CAZA1j025738 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 12 Feb 2008 11:35:21 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPUEsUfBAkMth2dsb2JhbACQOwEBAQgKKZsK X-IronPort-AV: E=Sophos;i="4.25,339,1199660400"; d="scan'208";a="22529043" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail4-smtp-sop.national.inria.fr with ESMTP; 12 Feb 2008 11:35:20 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id EA31F326BED for ; Tue, 12 Feb 2008 11:35:19 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id 3UloXt04sB+W for ; Tue, 12 Feb 2008 11:35:19 +0100 (CET) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id AB92132879D for ; Tue, 12 Feb 2008 11:35:19 +0100 (CET) Message-ID: <47B17667.2090907@fmf.uni-lj.si> Date: Tue, 12 Feb 2008 11:35:19 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: Caml Subject: Re: [Caml-list] type unsoundness with constraints and polymorphic variants References: <18352.43565.401296.820373@nyc-qws-r03.delacy.com> <20080212.132225.27792058.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20080212.132225.27792058.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 47B1765E.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 variants:01 ocaml:01 compiler:01 ocaml:01 formalized:01 compiler:01 polymorphic:01 typing:01 caml-list:01 commented:02 constraints:03 generally:04 xavier:06 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? Andrej