Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boutin, Réflexions sur les quotients, 1997.

M. Clochard, Preuves taillées en biseau, Vingthuitì emes Journées Francophones des Langages Applicatifs, 2017.

M. Clochard, J. C. Filliâtre, C. Marché, and A. Paskevich, Formalizing Semantics with an Automatic Program Verifier, 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE). Lecture Notes in Computer Science, pp.37-51, 2014.
DOI : 10.1007/978-3-319-12154-3_3
URL : https://hal.archives-ouvertes.fr/hal-01067197

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, ITP -3rd International Conference on Interactive Theorem Proving -2012, pp.83-98
DOI : 10.1007/978-3-642-32347-8_7

J. C. Filliâtre, One logic to use them allCADE-24), 24th International Conference on Automated Deduction, pp.1-20, 2013.

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verification, pp.1-16, 2014.

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

F. Palomo-lozano, I. Medina-bulo, and J. Alonso-jiménez, Certification of matrix multiplication algorithms. Strassen's algorithm in ACL2, Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp.283-298, 2001.

S. Srivastava, S. Gulwani, and J. S. Foster, From program verification to program synthesis, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.313-326, 2010.
DOI : 10.1145/1707801.1706337
URL : http://www.cs.umd.edu/~saurabhs/pubs/popl10-synthesis.pdf

R. Thiemann and A. Yamada, Matrices, jordan normal forms, and spectral radius theory, Archive of Formal Proofs, vol.2015, 2015.