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

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, 2012.
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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.148.395