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=1.2 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, SPF_SOFTFAIL 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 2BB94BBCA for ; Thu, 14 Feb 2008 10:00:56 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJ2Ss0eFBoIFh2dsb2JhbACQQQEBAQgKKZ1B X-IronPort-AV: E=Sophos;i="4.25,351,1199660400"; d="scan'208";a="7300848" Received: from rabbit.math.nagoya-u.ac.jp ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Feb 2008 10:00:51 +0100 Received: from localhost (millas [172.16.30.29]) by rabbit.math.nagoya-u.ac.jp (8.12.11/3.7W) with ESMTP id m1E90bxJ020577; Thu, 14 Feb 2008 18:00:37 +0900 (JST) Date: Thu, 14 Feb 2008 18:00:35 +0900 (JST) Message-Id: <20080214.180035.260790111.garrigue@math.nagoya-u.ac.jp> To: Andrej.Bauer@andrej.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Formal specifications of programming languages From: Jacques Garrigue In-Reply-To: <47B348F6.6010607@fmf.uni-lj.si> References: <47B33548.1010001@fmf.uni-lj.si> <4a051d930802131027o6459e7e7i6d35d4eb6e186eea@mail.gmail.com> <47B348F6.6010607@fmf.uni-lj.si> X-Mailer: Mew version 4.0.69 on Emacs 22.0.50 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 semantics:01 formalized:01 inference:01 semantics:01 inference:01 unspecified:01 wiki:01 wrote:01 caml-list:01 algorithm:01 modules:02 checking:02 checking:02 From: Andrej Bauer > Christopher L Conway wrote: > > But, Andrej, we don't even have an *informal* semantics. :-( You've > > got to walk before you run. > > Didn't Jacques say in a related post "Most of the type system is > formalized, but there is no single place to look at"? Jacques, does the > "type system" mean "type checking", "type inference", "operational > semantics", or what. Heck, I should just look up the papers. This is mostly about providing a formal type system (what you would call type checking) and prove that it admits principal types (so that an inference algorithm exists). Of course, for the modules system there is no inference (it still use core-language inference). Concerning the operational semantics, the reference manual is quite complete I believe. Of course some things are left unspecified, but this is actually part of the specification (you should be able to write programs without knowing the exact evaluation orer for instance.) > Maybe we should collect the relevant URLs and place them in the wiki. It > would be a start. I might do that. Good idea indeed. Jacques Garrigue