Wednesday, February 18, 2009

a shallow embedding of B set-theory in Coq

A message of Samuel Colin
Hi list,
for the past months I spent some effort upon the development of a shallow embedding of B set-theory in Coq[1]. The goal was two-fold:
- Validate, by implementing them, theorems of the B-Book, the "bible" of the B method[2]
- Have a prover for B based on what is described in the B-Book[3]

So, firstly, some links:

where this project is hosted, in a "bicoax" subdirectory of the Subversion trunk. for tarballs (you want the most recent one)
It should compile on a Linux platform with coq 8.2 (available as of very recently) and make, see the INSTALL file.

for the documentation generated by coqdoc (most of the comments refer to the place in the BBook of the corresponding theorem/definition).

In a nutshell and very broadly, I make this announce because it has entered a usable state, as showed by the Bmisc.v file of the project, containing two examples of small B projects whose all proof obligations are proved in BiCoax. BiCoax will be (and is already, in a sense) plugged back into the other tools of the BRILLANT platform so as to obtain a full toolchain for developing B projects.

What is implemented covers the first part of the B-Book: the first chapter (logical connectors), the second chapter (derived constructs, relations, functions) and half of the third chapter (mathematical constructs, up to and not including relative integers). Some constructs introduced in event-B were also added and I also put some eventB unicode notations with (hopefully) the correct priority as described by the Rodin D7 deliverable.

You can find an expanded version of this message here:
with more technical details.

This message was sent to the "BForum" mailing-list and the "Coq-club" mailing list.

only excerpts are available, but a lot of chapter 2 is visible

Samuel Colin

No comments: