Skip to Main content Skip to Navigation

Étude formelle d'algorithmes efficaces en algèbre linéaire

Maxime Dénès 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Formal methods have reached a degree of maturity leading to the design of general-purpose proof systems, enabling both to verify the correctness of complex software systems and to formalize advanced mathematics. However, the ease of reasoning on programs is often emphasized more than their efficient execution. The antagonism between these two aspects is particularly significant for computer algebra algorithms, whose correctness usually relies on elaborate mathematical concepts, but whose practical efficiency is an important matter of concern. This thesis develops approaches to the formal study and the efficient execution of programs in type theory, and more precisely in the proof assistant \coq{}. In a first part, we introduce a runtime environment enabling the native code compilation of such programs while retaining the generality and expressiveness of the formalism. Then, we focus on data representations and in particular on the formally verified and automatized link between proof-oriented and computation-oriented representations. Then, we take advantage of these techniques to study linear algebra algorithms, like Strassen's matrix product, Gaussian elimination or matrix canonical forms, including the Smith normal form for matrices over a Euclidean ring. Finally, we open the field of applications to the formalization and certified computation of homology groups of simplicial complexes arising from digital images.
Document type :
Complete list of metadatas

Cited literature [88 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Wednesday, February 12, 2014 - 10:07:08 PM
Last modification on : Thursday, March 5, 2020 - 5:34:40 PM
Long-term archiving on: : Tuesday, May 13, 2014 - 2:50:30 AM


Version validated by the jury (STAR)


  • HAL Id : tel-00945775, version 1



Maxime Dénès. Étude formelle d'algorithmes efficaces en algèbre linéaire. Autre [cs.OH]. Université Nice Sophia Antipolis, 2013. Français. ⟨NNT : 2013NICE4103⟩. ⟨tel-00945775⟩



Record views


Files downloads