Verified Computing in Homological Algebra

Arnaud Spiwack 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : L'objet de cette thèse est d'étudier les capacités du système Coq à mélanger démonstrations et programmes en pratique en essayant d'y implémenter une part du programme Kenzo, un outil de calcul formel en algèbre homologique. À cet effet, nous travaillons sous trois contrainte: nous voulons essayer de lire le programme comme une démonstration avec un contenu calculatoire, ces démonstrations doivent calculer efficacement et nous cherchons à éviter de dupliquer des morceaux de démonstration. Nous montrons dans un premier temps comment le soucis d'efficacité conduit à reconsidérer certains aspects des mathématiques traditionnelle. Nous proposons une abstraction catégorielle adaptée, qui répond à la fois à un soucis de clareté et au besoin de partager les démonstration quand c'est possible. Cette abstraction, bien que différente des propositions traditionnelles, permet de formuler les notions d'algèbre homologique dans un style proche de celui de Kenzo. Nous proposons par ailleurs des modifications au programme de Coq pour rendre les démonstrations plus confortables, et pour permettre d'écrire des programmes plus efficaces. La première modification permet d'utiliser des tactiques plus fines, souvent nécessaire quand l'utilisation des types dépendents se fait commune. La seconde permet d'utiliser les capacité du processeur pour faire des calculs plus efficaces sur des entiers. Pour finir nous proposons quelques pistes pour améliorer le partage et la clareté du code. Malheureusement, nous nous heurtons aux limites du système. Nous montrons ainsi que Coq ne tiens pas forcément ses promesses et qu'il y aura besoin de travaux théoriques pour comprendre comment lever ces limites.
Type de document :
Thèse
Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English
Liste complète des métadonnées


https://pastel.archives-ouvertes.fr/pastel-00605836
Contributeur : Arnaud Spiwack <>
Soumis le : lundi 4 juillet 2011 - 14:54:49
Dernière modification le : jeudi 9 février 2017 - 15:13:25
Document(s) archivé(s) le : lundi 12 novembre 2012 - 10:05:10

Identifiants

  • HAL Id : pastel-00605836, version 1

Collections

Citation

Arnaud Spiwack. Verified Computing in Homological Algebra. Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English. <pastel-00605836>

Partager

Métriques

Consultations de
la notice

508

Téléchargements du document

384