Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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
Document type :
Reports
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01412037
Contributor : José Grimm <>
Submitted on : Wednesday, December 7, 2016 - 6:13:45 PM
Last modification on : Thursday, January 11, 2018 - 4:48:52 PM
Long-term archiving on : Monday, March 20, 2017 - 6:12:37 PM

File

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

Identifiers

  • HAL Id : hal-01412037, version 1

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures. [Research Report] RR-8997, Inria Sophia Antipolis. 2016, pp.115. ⟨hal-01412037⟩

Share

Metrics

Record views

195

Files downloads

262