Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Ce document est la suite de deux rapports de recherche expliquant l'implémentation dans l'Assistant de Preuve Coq de la Théorie des Ensembles de Bourbaki. Il décrit le livre I, chapitre III, section 7 (limites inductives et projectives) et le débur du Livre I, chapitre IV (structues). Le code est disponible sur le site Web http://www-sop.inria.fr/marelle/gaia
Type de document :
Rapport
[Research Report] RR-8997, Inria Sophia Antipolis. 2016, pp.115
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01412037
Contributeur : José Grimm <>
Soumis le : mercredi 7 décembre 2016 - 18:13:45
Dernière modification le : jeudi 11 janvier 2018 - 16:48:52
Document(s) archivé(s) le : lundi 20 mars 2017 - 18:12:37

Fichier

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

Identifiants

  • HAL Id : hal-01412037, version 1

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures. [Research Report] RR-8997, Inria Sophia Antipolis. 2016, pp.115. 〈hal-01412037〉

Partager

Métriques

Consultations de la notice

151

Téléchargements de fichiers

184