Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers

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’œuvre 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és par Carlos Simpson. Ce rapport liste et commente toutes les définitions et théorèmes du Chapitre “En- sembles ordonnés, cardinaux, nombres entiers”. La version 9 de ce document décrit la bibliothèque à la fin de l'année 2017. Une partie des exercises a été résolue. Le code est disponible sur le site Web http://www-sop.inria.fr/marelle/gai
Type de document :
Rapport
[Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2017, pp.1-764
Liste complète des métadonnées

https://hal.inria.fr/inria-00440786
Contributeur : José Grimm <>
Soumis le : mercredi 29 novembre 2017 - 11:42:43
Dernière modification le : jeudi 11 janvier 2018 - 16:18:59

Fichier

RR7150v9.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00440786, version 9

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2017, pp.1-764. 〈inria-00440786v9〉

Partager

Métriques

Consultations de la notice

126

Téléchargements de fichiers

52