newsBRILLANT - News: BiCoax, a Coq library for B, is in the repository

 
 
Show feedback again
Latest News
B parsing is complete posted by scolin, Mon Apr 16 16:22:19 2012 - 0 replies
CSP||B tool for calculating control loop invariants posted by scolin, Mon Nov 30 18:01:23 2009 - 0 replies
BiCoax, a Coq library for B, is in the repository posted by scolin, Tue Sep 2 14:54:50 2008 - 0 replies
Alpha (debian) package : brillant-core posted by gmariano, Tue Jan 29 11:57:45 2008 - 1 reply

BiCoax, a Coq library for B, is in the repository

Item posted by Samuel Colin <scolin> on Tue Sep 2 14:54:50 2008.

Coq libraries for B have entered the BRILLANT project under the BiCoax name. These libraries are meant as a future replacement for BPhoX, as PhoX is not maintained anymore: this seems a good excuse to transfer BPhoX knowledge to Coq, whose longevity is more ensured.

At the moment, the content of BiCoax matches that of BPhoX in terms of defined operators and available theorems.

The part about translating from xml to BiCoax shall be added in the future when BiCoax has stabilised.

See the README in bicoax/ for more details.

Comments:

No messages in BiCoax, a Coq library for B, is in the repository

 

Start a New Thread:

You could post if you were logged in
Show feedback again

Back to the top


Powered by Savane 3.1-cleanup