Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. I: Theory of sets

MaRDI QIDQ3075244zbMATH OpenFDO

Authors José Grimm

Publication date 10 February 2011

Full work available at URL http://jfr.cib.unibo.it/article/view/1899

zbMATH Keywords

Bourbaki's Elements of MathematicsCoq proof assistantformalization of set theoryGaia softwareZermelo's theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Recommendations

• Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
• scientific article; zbMATH DE number 2080010
• An experimental library of formalized mathematics based on the univalent foundations
• Mathematical Knowledge Management
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Cited in

(4)

• From Sets to Bits in Coq
• scientific article; zbMATH DE number 2080010 (Why is no real title available?)
• Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
• A reassessment of cantorian abstraction based on the -operator

Describes a project that uses

Uses Software

• Coq
• gaia

This page was built for publication: Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. I: Theory of sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075244)