Yet Another Deep Embedding of B:Extending de Bruijn Notations

Eric Jaeger (1, 2) , Thérèse Hardin (2)

1 DCSSI/SDS/LTI - Laboratoire des Technologies de l'Information
2 SPI - Sémantiques, preuves et implantation

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 sets and maps, the use of induction principles, and the introduction of a new de Bruijn notation providing solutions to various problems related to the mechanisation of languages and logics.

Mots clés: Formal Methods; Deep Embedding; de Bruijn Notation

Domaines: Logique en informatique [cs.LO]

Eric Jaeger, Thérèse Hardin. Yet Another Deep Embedding of B:Extending de Bruijn Notations. 2009. ⟨hal-00363348⟩