Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
In: Journal of Formalized Reasoning, Jg. 9 (2016), Heft 2, S. 1-52
Online
academicJournal
Zugriff:
This paper describes a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant. In a first paper published in this journal, we presented the axioms and basic constructions (corresponding to a part of the first two chapters of book I, theory of sets). We discuss here the set of integers (third chapter of book I, theory of set), the sets Z and Q (first chapter of book II, Algebra) and the set of real numbers (Chapter 4 of book III, General topology). We start with a comparison of the Bourbaki approach, the Coq standard library, and the Ssreflect library, then present our implementation.
Titel: |
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
|
---|---|
Autor/in / Beteiligte Person: | Grimm, José |
Link: | |
Zeitschrift: | Journal of Formalized Reasoning, Jg. 9 (2016), Heft 2, S. 1-52 |
Veröffentlichung: | University of Bologna, 2016 |
Medientyp: | academicJournal |
ISSN: | 1972-5787 (print) |
DOI: | 10.6092/issn.1972-5787/4771 |
Schlagwort: |
|
Sonstiges: |
|