A. Aguirre, Towards a provably correct encoding from F* to SMT. Master's thesis, 2016.

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Thery et al., A modular integration of SAT/SMT solvers to Coq through proof witnesses, Certified Programs and Proofs, vol.7086, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti : a logical framework based on the ??-calculus modulo theory, 2016.

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Expressing theories in the ??-calculus modulo theory and in the Dedukti system, 22nd International Conference on Types for Proofs and Programs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01441751

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3 : Shepherd your herd of provers, International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let's verify this with Why3, International Journal on Software Tools for Technology Transfer (STTT), vol.17, issue.6, pp.709-727, 2015.

S. Böhme and T. Weber, Fast LCF-style proof reconstruction for Z3, Interactive Theorem Proving, vol.6172, pp.179-194, 2010.

R. Cauderlier and P. Halmagrand, Checking Zenon modulo proofs in Dedukti, Proof eXchange for Theorem Proving, vol.186, pp.57-73, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01171360

E. Contejean, Coccinelle, a Coq library for rewriting, Types, 2008.

S. Dailler, C. Marché, and Y. Moy, Lightweight interactive proving inside an automatic program verifier, Formal Integrated Development Environments, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01936302

D. Greenaway, Automated proof-producing abstraction of C code, CSE, 2015.

D. Greenaway, J. Lim, J. Andronick, and G. Klein, Don't sweat the small stuff : Formal verification of C code without the pain, Programming Language Design and Implementation, pp.429-439, 2014.

B. Grégoire, L. Théry, and B. Werner, A computational approach to Pocklington certificates in type theory, Functional and Logic Programming, vol.3945, pp.97-113, 2006.

R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer et al., The essence of higher-order concurrent separation logic, Programming Languages and Systems, vol.10201, pp.696-723, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01633133

N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multimonadic effects in F*, Principles of Programming Languages, pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793