-
Formal study of efficient algorithms in linear algebra
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... -
Programming with Dependent Types in Coq: a Study of Square Matrices
Unpublished, but worth reading. -
Extraction of Certified Functional Code from Inductive Specifications
Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have... -
Coqcots & Pycots: non-stopping components for safe dynamic reconfiguration
International audience -
A Vernacular for Coherent Logic
International audience -
Implantation de l'algorithme de Stalmarck dans le cadre de la cooperation COQ...
Stage de fin d'etudes. Rapport de stage. -
Certification des preuves de terminaison par interprétations polynomiales
Stage de DEA. Rapport de stage. -
Définition de la classe de réécriture à intégrer
Rapport de contrat. -
Proposition d'architecture du moteur de test de conversion
Rapport de contrat. -
Prototype d'extension du système Coq
Rapport de contrat.
