Bedwyr 1.0
 David Baelde
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  David Baelde <david.baelde@g...> 
Subject:  Bedwyr 1.0 
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 modelchecking 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 picalculus. Other examples include type systems, games, logics, etc. But another interest for the camllist readers might be the reusable core components of Bedwyr, notably higherorder 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 proofsearch 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) Higherorder abstract syntax can be supported at a logical level by using termlevel lambdabinders, the nablaquantifier, higherorder 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 picalculus (operational semantics, bisimulation, trace analyses and modal logics), the spicalculus (operational semantics), valuepassing CCS, the lambdacalculus, winning strategies for games, and various other model checking problems. These examples should also show the ease with which a new rulebased 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 opensource project, we welcome contributions in the form of example applications and also new features from others.