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.
Domaines
Logiciel mathématique [cs.MS]
Origine : Fichiers produits par l'(les) auteur(s)