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.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs