The Coq mailing list

[Samuel Colin <scolin-lists AT hivernal.org>]

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:

https://gna.org/projects/brillant

where this project is hosted, in a "bicoax" subdirectory of the
Subversion trunk.

http://download.gna.org/brillant/snapshots/ 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.

http://download.gna.org/brillant/snapshots/bicoax-html/
and
http://download.gna.org/brillant/snapshots/bicoax-html/toc.html

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:
http://download.gna.org/brillant/snapshots/BiCoax-announce
with more technical details.

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

References:
[1] http://coq.inria.fr/
[2] http://en.wikipedia.org/wiki/B-Method
 or http://fr.wikipedia.org/wiki/Méthode_B
[3] http://books.google.com/books?id=Cbx9A85TrOYC
    only excerpts are available, but a lot of chapter 2 is visible

-- 
Samuel Colin
E-mail: 
scolin AT hivernal.org
Informations: http://hivernal.org/static/about/