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

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), pp.52. 〈https://jfr.unibo.it/article/view/4771〉. 〈10.6092/issn.1972-5787/4771〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01415375
Contributeur : José Grimm <>
Soumis le : lundi 19 décembre 2016 - 14:53:05
Dernière modification le : vendredi 12 janvier 2018 - 01:48:57
Document(s) archivé(s) le : mardi 21 mars 2017 - 09:46:10

Fichier

jfra2-v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), pp.52. 〈https://jfr.unibo.it/article/view/4771〉. 〈10.6092/issn.1972-5787/4771〉. 〈hal-01415375〉

Partager

Métriques

Consultations de la notice

221

Téléchargements de fichiers

44