[TYPES/announce] Bedwyr 1.0

[David Baelde]

Dear colleagues,

We would like to announce the first release of Bedwyr, an extended
logic programming language that allows model-checking directly on
syntactic expressions possibly containing bindings.

Bedwyr allows simple and declarative relational specifications of
various systems, and provides a simple approach to reason on them.
Examples of applications include type systems, process calculi, games,
logics, etc.

Bedwyr makes use of a simple form of tabling to support proof search
for inductive and co-inductive specifications, typically allowing
bisimulation checking for non-terminating processes.

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.