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 2C268BBC1 for ; Wed, 13 Feb 2008 20:44:24 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAACLXskfBAkMth2dsb2JhbACQQAEBAQgKKZ0i X-IronPort-AV: E=Sophos;i="4.25,347,1199660400"; d="scan'208";a="7282639" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 13 Feb 2008 20:44:24 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 77E2F32FB42; Wed, 13 Feb 2008 20:44:23 +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 bIZ-s1CyKS9p; Wed, 13 Feb 2008 20:44:23 +0100 (CET) Received: from [192.168.1.113] (BSN-77-148-136.static.dsl.siol.net [193.77.148.136]) (Authenticated sender: bauer) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 2086A32FA59; Wed, 13 Feb 2008 20:44:23 +0100 (CET) Message-ID: <47B348F6.6010607@fmf.uni-lj.si> Date: Wed, 13 Feb 2008 20:45:58 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 1.5.0.14pre (X11/20071023) MIME-Version: 1.0 To: Christopher L Conway Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Formal specifications of programming languages References: <47B33548.1010001@fmf.uni-lj.si> <4a051d930802131027o6459e7e7i6d35d4eb6e186eea@mail.gmail.com> In-Reply-To: <4a051d930802131027o6459e7e7i6d35d4eb6e186eea@mail.gmail.com> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 semantics:01 formalized:01 inference:01 semantics:01 wiki:01 wrote:01 caml-list:01 checking:02 jacques:03 jacques:03 languages:03 programming:03 informal:04 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. Maybe we should collect the relevant URLs and place them in the wiki. It would be a start. I might do that. Andrej