Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2009

Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

Résumé

We believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter ``Theory of Sets''. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia . Version one was released in July 2009, version 2 in December 2009, version 3 in March 2010. There are small differences, marked in footnotes.
Fichier principal
Vignette du fichier
RR-6999-V3.pdf (1 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00408143 , version 1 (29-07-2009)
inria-00408143 , version 2 (08-12-2009)
inria-00408143 , version 3 (30-03-2010)
inria-00408143 , version 4 (02-12-2010)
inria-00408143 , version 5 (14-12-2011)
inria-00408143 , version 6 (31-10-2013)
inria-00408143 , version 7 (04-12-2018)

Identifiants

  • HAL Id : inria-00408143 , version 3

Citer

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. [Research Report] RR-6999, 2009, pp.209. ⟨inria-00408143v3⟩
685 Consultations
2734 Téléchargements

Partager

Gmail Facebook X LinkedIn More