Verified Computing in Homological Algebra ; Calculs vérifiés en algèbre homologique
In: https://pastel.hal.science/pastel-00605836 ; Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English. ⟨NNT : ⟩, 2011
Online
Hochschulschrift
Zugriff:
The object of this thesis is the study of the ability of the Coq system to mix proofs and programs in practice. Our approach consists in implementing part of the program Kenzo, a computer algebra tool for homological algebra under some constraint. We want to be able to read the program as a proof with a computational content, these proofs much compute efficiently, and we try to avoid duplication of proofs or part thereof. We show, first, how the requirement of efficiency leads to revise some aspects of traditional mathematics. We propose a suitable categorical abstraction, both for clarity and to avoid duplications. This abstraction, though different from what is customary in mathematics, allow to formulate the constructs of homological algebra in a style much like that of Kenzo. We propose, then, modifications to the Coq programm. A first one to make proofs more convenient, by allowing the use of more fine grain tactics which are often necessary when dependent types are common. The second modification to leverage the arithmetical abilities of the processor to compute more efficiently on integers. Finally, we propose some leads to improve both sharing and clarity of the proofs. Unfortunately, they push the system beyond its limits. Hence, we show that Coq is not always up to its promises and that theoretical works will be necessary to understand how these limits can be relaxed. ; 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 ...
Titel: |
Verified Computing in Homological Algebra ; Calculs vérifiés en algèbre homologique
|
---|---|
Autor/in / Beteiligte Person: | Spiwack, Arnaud ; Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) ; Types, Logic and computing (TYPICAL) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Ecole Polytechnique, X ; Werner(benjamin.werner@inria.fr), Benjamin |
Link: | |
Zeitschrift: | https://pastel.hal.science/pastel-00605836 ; Algebraic Topology [math.AT]. Ecole Polytechnique X, 2011. English. ⟨NNT : ⟩, 2011 |
Veröffentlichung: | HAL CCSD, 2011 |
Medientyp: | Hochschulschrift |
Schlagwort: |
|
Sonstiges: |
|