Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
From MaRDI portal
Publication:5195277
DOI10.6092/issn.1972-5787/4771zbMath1451.68339OpenAlexW2570826447MaRDI QIDQ5195277
Publication date: 18 September 2019
Full work available at URL: https://doaj.org/article/b7e37bc9ffcf459692a7c8f59465a3aa
Mechanization of proofs and logical operations (03B35) Set theory (03E99) Formalization of mathematics in connection with theorem provers (68V20)
Uses Software
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