Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers (Q5195277): Difference between revisions

Latest revision as of 11:04, 20 July 2024

scientific article; zbMATH DE number 7106511

Language	Label	Description	Also known as
English	Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers	scientific article; zbMATH DE number 7106511

Statements

0 references

0 references

18 September 2019

0 references

zbMATH Keywords

Coq

0 references

Bourbaki

0 references

sets

0 references

integers

0 references

rational numbers

0 references

real numbers

0 references

describes a project that uses

0 references

0 references

0 references

MaRDI publication profile

0 references

full work available at URL

https://doaj.org/article/b7e37bc9ffcf459692a7c8f59465a3aa

0 references

title

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

0 references

cites work

Formalization of real analysis: a survey of proof assistants and libraries

0 references

Q5565097

0 references

Q4040889

0 references

Q5522002

0 references

Construction of Real Algebraic Numbers in Coq

0 references

Q4117362

0 references

Packaging Mathematical Structures

0 references

Q3075246

0 references

Q3075244

0 references

Types for Proofs and Programs

0 references

Exact arithmetic on the Stern-Brocot tree

0 references

Computer theorem proving in mathematics

0 references

Identifiers

zbMATH Open document ID

1451.68339

0 references

DOI

10.6092/issn.1972-5787/4771

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5195277

@@ label / en / label / en @@
+Implementation of Bourbaki's Elements of   Mathematics in Coq:  Part Two, From Natural Numbers to Real Numbers
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doaj.org/article/b7e37bc9ffcf459692a7c8f59465a3aa
+Normal rank
@@ Property / OpenAlex ID @@
+W2570826447
@@ Property / OpenAlex ID: W2570826447 / rank @@
+Normal rank
@@ Property / title @@
+Implementation of Bourbaki's Elements of   Mathematics in Coq:  Part Two, From Natural Numbers to Real Numbers (English)
+Normal rank
@@ Property / cites work @@
+Formalization of real analysis: a survey of proof assistants and libraries
+Normal rank
@@ Property / cites work @@
+Q5565097
@@ Property / cites work: Q5565097 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4040889
@@ Property / cites work: Q4040889 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5522002
@@ Property / cites work: Q5522002 / rank @@
+Normal rank
@@ Property / cites work @@
+Construction of Real Algebraic Numbers in Coq
@@ Property / cites work: Construction of Real Algebraic Numbers in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4117362
@@ Property / cites work: Q4117362 / rank @@
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075246
@@ Property / cites work: Q3075246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075244
@@ Property / cites work: Q3075244 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Exact arithmetic on the Stern-Brocot tree
@@ Property / cites work: Exact arithmetic on the Stern-Brocot tree / rank @@
+Normal rank
@@ Property / cites work @@
+Computer theorem proving in mathematics
@@ Property / cites work: Computer theorem proving in mathematics / rank @@
+Normal rank