Yet Another Deep Embedding of B:Extending de Bruijn Notations
Eric Jaeger (LIP6, Dcssi/SDS/Lti), Th\'er\`ese Hardin (LIP6)
TL;DR
This paper introduces Bicoq3, a deep embedding of the B system in Coq, emphasizing advanced representation techniques, induction principles, and a novel de Bruijn notation to facilitate language and logic mechanisation.
Contribution
It presents a new de Bruijn notation and detailed embedding strategies for the B system in Coq, enhancing formal language mechanisation.
Findings
Improved representation of sets and maps in Coq
New de Bruijn notation addresses mechanisation challenges
Enhanced induction principles for formal proofs
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Homotopy and Cohomology in Algebraic Topology · Computability, Logic, AI Algorithms