A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds et al., Program logics for certified compilers, 2014.
DOI : 10.1017/CBO9781107256552

G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development -Coq'Art : The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/978-3-642-02959-2_10

A. Chlipala, Certified Programming with Dependent Types, 2011.

G. Gonthier, Formal proof ? the four-color theorem . Notices of the, 2008.

J. Harrison, HOL Light: An Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, 42nd ACM symposium on Principles of Programming Languages, 2015.
DOI : 10.1145/2775051.2676966
URL : https://hal.archives-ouvertes.fr/hal-01078386

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014, 7th International Symposium on Leveraging Applications, 7th International Symposium on Leveraging Applications, p.16, 2016.
DOI : 10.1007/978-3-662-46681-0_53
URL : https://hal.archives-ouvertes.fr/hal-01344110

D. Kästner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt et al., Closing the gap -the formally verified optimizing compiler CompCert, Safety-critical Systems Symposium 2017, 2017.

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

M. Mauny, Le langage Caml. Techniques pour l'ingénieur, 2017.

W. John, P. C. Mccormick, and . Chapin, Building High Integrity Applications with SPARK, 2015.

R. Milner, Lcf: A way of doing proofs with a machine, Lecture Notes in Computer Science, vol.74, pp.146-159, 1979.
DOI : 10.1007/3-540-09526-8_11

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL : A Proof Assistant for Higher-order Logic, 2002.
DOI : 10.1007/3-540-45949-9