Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers

DOI10.6092/issn.1972-5787/4771zbMath1451.68339OpenAlexW2570826447MaRDI QIDQ5195277

José Grimm

Publication date: 18 September 2019

Full work available at URL: https://doaj.org/article/b7e37bc9ffcf459692a7c8f59465a3aa

zbMATH Keywords

setsreal numbersintegersBourbakiCoqrational numbers

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• Coq/SSReflect
• gaia

Cites Work

• Computer theorem proving in mathematics
• Exact arithmetic on the Stern-Brocot tree
• Construction of Real Algebraic Numbers in Coq
• Formalization of real analysis: a survey of proof assistants and libraries
• Packaging Mathematical Structures
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers