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 16 Apr 2012 04:22:19 PM UTC - 0 replies
CSP||B tool for calculating control loop invariants posted by scolin, Mon 30 Nov 2009 06:01:23 PM UTC - 0 replies
BiCoax, a Coq library for B, is in the repository posted by scolin, Tue 02 Sep 2008 02:54:50 PM UTC - 0 replies
Alpha (debian) package : brillant-core posted by gmariano, Tue 29 Jan 2008 11:57:45 AM UTC - 1 reply
New jabber chatroom / nouveau salon jabber posted by scolin, Mon 28 Jan 2008 04:51:22 PM UTC - 0 replies
[Submit News]
[13 news in archive]

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

Item posted by Samuel Colin <scolin> on Tue 02 Sep 2008 02:54:50 PM UTC.

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