Towards a provably correct encoding from F* to SMT. Master's thesis, 2016. ,
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
Dedukti : a logical framework based on the ??-calculus modulo theory, 2016. ,
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
Why3 : Shepherd your herd of provers, International Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
Let's verify this with Why3, International Journal on Software Tools for Technology Transfer (STTT), vol.17, issue.6, pp.709-727, 2015. ,
Fast LCF-style proof reconstruction for Z3, Interactive Theorem Proving, vol.6172, pp.179-194, 2010. ,
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
Coccinelle, a Coq library for rewriting, Types, 2008. ,
Lightweight interactive proving inside an automatic program verifier, Formal Integrated Development Environments, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01936302
Automated proof-producing abstraction of C code, CSE, 2015. ,
Don't sweat the small stuff : Formal verification of C code without the pain, Programming Language Design and Implementation, pp.429-439, 2014. ,
A computational approach to Pocklington certificates in type theory, Functional and Logic Programming, vol.3945, pp.97-113, 2006. ,
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
Dependent types and multimonadic effects in F*, Principles of Programming Languages, pp.256-270, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01265793