Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures
Résumé
This document is a follow-up to two research reports
explaining the implementation in the Coq proof assistant of the
Theory of Sets of Bourbaki. It explains Book I, Chapter III, Section
7 (Inverse limits and direct limits) and the start of Book I,
Chapter IV (structures).
The code is available on the Web, under
http://www-sop.inria.fr/marelle/gaia
Ce document est la suite de deux rapports de recherche
expliquant l'implémentation dans l'Assistant de Preuve Coq de la
Théorie des Ensembles de Bourbaki. Il décrit le livre I, chapitre III,
section 7 (limites inductives et projectives) et le débur du Livre
I, chapitre IV (structues).
Le code est disponible sur le site Web
http://www-sop.inria.fr/marelle/gaia
Domaines
Logiciel mathématique [cs.MS]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...