Skip to Main content Skip to Navigation

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
Abstract : 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.
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download
Contributor : Arnaud Spiwack Connect in order to contact the contributor
Submitted on : Monday, July 4, 2011 - 2:54:49 PM
Last modification on : Friday, February 4, 2022 - 3:18:39 AM
Long-term archiving on: : Monday, November 12, 2012 - 10:05:10 AM


  • HAL Id : pastel-00605836, version 1



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



Record views


Files downloads