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.3 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 9FDDDBC76 for ; Wed, 1 Nov 2006 14:02:30 +0100 (CET) Received: from nz-out-0102.google.com (nz-out-0102.google.com [64.233.162.200]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id kA1D2TLq009757 for ; Wed, 1 Nov 2006 14:02:30 +0100 Received: by nz-out-0102.google.com with SMTP id 13so1734375nzp for ; Wed, 01 Nov 2006 05:02:29 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=KC4w9FnjsDOETDeJUJdFyfabcCkswbHOP5CXzQ09AHDIzYBAT+fz5ZQcjXctjxQ8RNM2k2GQwNH0FdoFa7GJCkDlzNwz9wn6xfybcKoS51QdmkMtj8gGEGB3TjsIU6BsJNneLPo3XDRZVwmXRZHwIZaPqrNOq+9nyfXl1HiO2Sc= Received: by 10.35.31.14 with SMTP id i14mr8790405pyj; Wed, 01 Nov 2006 05:02:28 -0800 (PST) Received: by 10.35.76.7 with HTTP; Wed, 1 Nov 2006 05:02:28 -0800 (PST) Message-ID: <53c655920611010502v257bbebq627ed4c91ab17fce@mail.gmail.com> Date: Wed, 1 Nov 2006 14:02:28 +0100 From: "David Baelde" Reply-To: david.baelde@ens-lyon.org To: Ocaml Subject: Bedwyr 1.0 MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline X-j-chkmail-Score: MSGID : 45489AE5.001 on discorde : j-chkmail score : X : 0/20 1 X-Miltered: at discorde with ID 45489AE5.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 bindings:01 bisimulation:01 logics:01 higher-order:01 unification:01 model:01 ocaml:01 computations:01 model:01 formalize:01 semantics:01 higher-order:01 syntax:01 unification:01 Hi list, We would like to announce the first release of a new system written in OCaml. Bedwyr is an extended logic programming language that allows model-checking directly on syntactic expressions possibly containing bindings. We believe that it's an interesting tool for computer scientists, as it allows simple reasoning on declarative specifications, with several good examples, notably bisimulation checking for the pi-calculus. Other examples include type systems, games, logics, etc. But another interest for the caml-list readers might be the re-usable core components of Bedwyr, notably higher-order pattern unification and term indexing. Although we don't distribute these separately, I'd be happy to do so if anybody is interested. You will find a general description of Bedwyr below this message. More details can be found on Bedwyr website: http://slimmer.gforge.inria.fr/bedwyr/ Sincerely, Bedwyr developers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Bedwyr A proof-search approach to model checking http://slimmer.gforge.inria.fr/bedwyr/ Bedwyr is a programming framework written in OCaml that facilitates natural and perspicuous presentations of rule oriented computations over syntactic expressions and that is capable of model checking based reasoning over such descriptions. Bedwyr is in spirit a generalization of logic programming. However, it embodies two important recent observations about proof search: (1) It is possible to formalize both finite success and finite failure in a sequent calculus; proof search in such a proof system can capture both may and must behavior in operational semantics specifications. (2) Higher-order abstract syntax can be supported at a logical level by using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions; these features allow reasoning directly on expressions containing bound variables. The distribution of Bedwyr includes illustrative applications to the finite pi-calculus (operational semantics, bisimulation, trace analyses and modal logics), the spi-calculus (operational semantics), value-passing CCS, the lambda-calculus, winning strategies for games, and various other model checking problems. These examples should also show the ease with which a new rule-based system and particular questions about its properties can be be programmed in Bedwyr. Because of this characteristic, we believe that the system can be of use to people interested in the broad area of reasoning about computer systems. The present distribution of Bedwyr has been developed by the following individuals: David Baelde & Dale Miller (INRIA & LIX/Ecole Polytechnique) Andrew Gacek & Gopalan Nadathur (University of Minneapolis) Alwen Tiu (Australian National University and NICTA). In the spirit of an open-source project, we welcome contributions in the form of example applications and also new features from others.