Activité

Je suis actuellement doctorant en informatique. Je travaille sur la formalisation des mathématiques avec l'extension SSReflect de l'assistant de preuve Coq. Ma thèse porte principalement sur la formalisation des trois résultats suivants :

• la forme normale de Jordan d'une matrice (algèbre linéaire)
• le théorème de Bolzano-Weierstrass (topologie générale)
• le théorème de Perron-Frobenius (algèbre linéaire)

• these.pdf

Fichiers sources

• Pré-requis : pour compiler les fichiers sources, vous aurez besoin d'installer :
• coq-8.4pl2 ou 3
• feit_thomson v2.0
• Développement :
• Cano_linear_algebra-topology.tar.gz

Documentation

Liens

• Coq
• SSReflect
• CoqEAL

Contact

guillaume.cano@inria.fr