Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Formalized Reasoning Année : 2016

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

Résumé

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.
Fichier principal
Vignette du fichier
jfra2-v2.pdf (664.61 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01415375 , version 1 (19-12-2016)

Identifiants

Citer

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. Journal of Formalized Reasoning, 2016, 9 (2), pp.52. ⟨10.6092/issn.1972-5787/4771⟩. ⟨hal-01415375⟩
262 Consultations
392 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More