Point-Free, Set-Free Concrete Linear Algebra

Résumé : On présente une formalisation en Coq de l'algèbre linéaire où tous les objets sont représentés par des matrices, y compris les sous-espaces. Ce développement a été utilisé pour élaborer la formalisation des éléments de théorie de la représentation nécessaires à la prévue du théorème de Feit-Thompson.
Type de document :
Communication dans un congrès
Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk. Interactive Theorem Proving - ITP 2011, Aug 2011, Berg en Dal, Netherlands. Springer, 6898, pp.103-118, 2011, Lecture Notes in Computer Science; Interactive Theorem Proving - Second International Conference, ITP 2011. <10.1007/978-3-642-22863-6_10>
Liste complète des métadonnées


https://hal.inria.fr/hal-00805966
Contributeur : Georges Gonthier <>
Soumis le : vendredi 29 mars 2013 - 15:03:50
Dernière modification le : vendredi 29 mars 2013 - 15:51:27
Document(s) archivé(s) le : dimanche 30 juin 2013 - 04:00:42

Fichier

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

Identifiants

Collections

Citation

Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk. Interactive Theorem Proving - ITP 2011, Aug 2011, Berg en Dal, Netherlands. Springer, 6898, pp.103-118, 2011, Lecture Notes in Computer Science; Interactive Theorem Proving - Second International Conference, ITP 2011. <10.1007/978-3-642-22863-6_10>. <hal-00805966>

Partager

Métriques

Consultations de
la notice

365

Téléchargements du document

292