Yet Another Deep Embedding of B:Extending de Bruijn Notations

Eric Jaeger, Thérèse Hardin

We present Bicoq3, a deep embedding of the B system in Coq, focusing on the technical aspects of the development. The main subjects discussed are related to the representation of s…