1 view

Skip to first unread message

Nov 1, 2006, 8:31:49 AM11/1/06

to Ocaml

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.

_______________________________________________

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu