BiCoax

Le post qui suit est technique, m'en fous, c'est moi que j'écris c'que j'veux sur eum'blog.

BiCoax est une bibliothèque Coq qui définit les constructions de la méthode B selon des constructions Coq. En gros on exprime la sémantique de B via ce que permet Coq, sous la forme d'un plongement léger. Ceci au contraire d'une approche de type «plongement profond» privilégiée par une bibliothèque BiCoq qui est un peu l'arlésienne parce qu'on ne peut l'obtenir nulle part. Que c'est beau cette culture du secret dans le microcosme de la méthode B...

Pourquoi je parle de tout ça ? Parce que je me suis occupé de la développer, sur la base d'une approche déjà existante mais qui souffre désormais de l'absence de maintenance du prouveur sur lequel elle est basée. Pour ceux que ça intéresse (qui doivent se compter sur les doigts d'un manchot), c'est par là.

-------
What follows is somewhat technical, whatever, that's my blog, I post what I want to post, goddamnit.

BiCoax is a Coq library defining B method constructs in terms of Coq constructs. More or less it's expressing B semantics through what Coq allows, under a shallow embedding. This is opposed to a "deep embedding" approach used by the BiCoq library which is not available anywhere. How cute, this habit of secrecy in the B community...

Why am I speaking about this ? Because I'm the one who developed it, on the base of an existing approach crippled by the prover it is based on, which is unmaintained. For those interested (who are probably as numerous as the the fingers of a penguin - note: it was one of the possible translations :-P ), take a look here.