Yet Another Deep Embedding of B:Extending de Bruijn Notations

Simple item page
dc.creatorJaeger, Eric
dc.creatorHardin, Thérèse
dc.date2009-02-23
dc.date.accessioned2026-07-07T12:45:36Z
dc.date.available2026-07-07T12:45:36Z
dc.descriptionWe 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.
dc.description16 pages
dc.identifierhttps://arxiv.org/abs/0902.3865
dc.identifierhttp://arxiv.org/abs/0902.3865
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/221135
dc.subjectLogic in Computer Science
dc.titleYet Another Deep Embedding of B:Extending de Bruijn Notations
dc.typetext

Files

Collections

arXiv