Skip to Main content Skip to Navigation
Reports

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

José Grimm 1
Abstract : 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. Version 4 is based on the Coq ssreflect library. There are small differences, marked in footnotes.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00408143
Contributor : José Grimm Connect in order to contact the contributor
Submitted on : Thursday, December 2, 2010 - 11:35:42 AM
Last modification on : Thursday, January 24, 2019 - 4:57:19 PM
Long-term archiving on: : Friday, December 2, 2016 - 8:51:04 PM

File

RR-6999-v4.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00408143, version 4

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. [Research Report] RR-6999, 2009, pp.229. ⟨inria-00408143v4⟩

Share

Metrics

Record views

575

Files downloads

2448