Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Nous pensons qu'il est possible de mettre dans un ordinateur l'ensemble de l'oeuvre de Bourbaki. L'un des objectifs du projet Gaia concerne l'algèbre homologique (théorie et algorithmes); dans une première étape nous voulons implémenter les neuf chapitres du livre Algèbre. Au préalable, il faut implémenter la théorie des ensembles. Nous utilisons l'Assistant de Preuve Coq; les choix fondamentaux et axiomes sont ceux proposées par Carlos Simpson. Ce rapport liste et commente toutes les définitions et théorèmes du Chapitre théorie des ensembles. Presque tous les exercices ont été résolus. Le code est disponible sur le site Web http://www-sop.inria.fr/marelle/gaia
Type de document :
Rapport
[Research Report] RR-6999, INRIA. 2013, pp.205
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00408143
Contributeur : José Grimm <>
Soumis le : jeudi 31 octobre 2013 - 16:36:13
Dernière modification le : jeudi 11 janvier 2018 - 16:40:42
Document(s) archivé(s) le : samedi 1 février 2014 - 04:29:58

Fichier

RR-6999-v6.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00408143, version 6

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. [Research Report] RR-6999, INRIA. 2013, pp.205. 〈inria-00408143v6〉

Partager

Métriques

Consultations de la notice

515

Téléchargements de fichiers

346