From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3K9OG45021066 for ; Fri, 20 Apr 2012 11:24:17 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiwFAFwqkU/Y5v4vmGdsb2JhbABDgxyCS5gUk0EiAQEBAQEICQ0HFCeCCQEBBSMPAQVAARALDQsCAgUWCwICCQMCAQIBRQYNCAEBiAoBC6djkyMEgS+OIIEYBIhhjRiFdCKNHQ X-IronPort-AV: E=Sophos;i="4.75,452,1330902000"; d="scan'208";a="140909666" Received: from unknown (HELO amout07.alpha-mail.net) ([216.230.254.47]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 20 Apr 2012 11:24:15 +0200 Received: from webarc04.alpha-mail.jp (webarc04 [216.230.254.84]) by amout07.alpha-mail.net with ESMTP id q3K9O7V2017691; Fri, 20 Apr 2012 18:24:08 +0900 X-Virus-Scanned: amavisd-new at Alpha-Mail Out Received: from ltsub01.alpha-mail.net (ltsub01 [216.230.254.29]) by webarc04.alpha-mail.jp (Postfix) with ESMTP id 106821C080D6; Fri, 20 Apr 2012 18:24:02 +0900 (JST) Received: from [192.168.0.110] (196.62.205.61.west.global.crust-r.net [61.205.62.196]) by ltsub01.alpha-mail.net (Alpha-mail) with ESMTP id 31A6E3B80B4; Fri, 20 Apr 2012 18:24:07 +0900 (JST) Message-ID: <4F912B3C.9040409@itpl.co.jp> Date: Fri, 20 Apr 2012 18:24:12 +0900 From: Satoshi Ogasawara User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120327 Thunderbird/11.0.1 MIME-Version: 1.0 To: =?UTF-8?B?RGFuaWVsIELDvG56bGk=?= Cc: caml-list@inria.fr References: <4F8D9D0E.1040007@itpl.co.jp> <4F8E1FF4.5070702@itpl.co.jp> <4F8EA91C.3060001@itpl.co.jp> <2B372C89CE4F408688B67B090FA5105C@erratique.ch> <4F8EFC34.7080906@itpl.co.jp> <4F8FD3EB.5050307@itpl.co.jp> <4F900CCD.5050102@itpl.co.jp> <2B7FE930300F440ABE0F439A3418222C@erratique.ch> In-Reply-To: <2B7FE930300F440ABE0F439A3418222C@erratique.ch> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] [ANN] PEC ver. 1.1 (2012/04/19 23:09), Daniel Bünzli wrote: >> Do you have any experience to proof a theorem against event combination term >> by using above axiom and event combinators semantics? I'm interested in this >> kind of reasoning. > > In this post I use the semantics and equational reasoning to understand why something doesn't happen. > > https://sympa-roc.inria.fr/wws/arc/caml-list/2009-12/msg00054.html > > (you may have to read the whole thread to fully understand the example). Thank you for your information. I like this kind of strict reasoning. I'd like to add some semantics to PEC, too. Any way, thank you for your educational discussion! Best Regards, Ogasawara