K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, pp.445-459, 2013.
DOI : 10.1109/SP.2013.37
URL : https://hal.archives-ouvertes.fr/hal-00863373

L. Bulwahn, A. Krauss, F. Haftmann, L. Erkök, and J. Matthews, Imperative Functional Programming with Isabelle/HOL, Theorem Proving in Higher Order Logics (TPHOLs), pp.134-149, 2008.
DOI : 10.1007/978-3-540-74591-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.176.4954

A. Charguéraud, Characteristic formulae for the verification of imperative programs, International Conference on Functional Programming (ICFP), pp.418-430, 2011.

A. Charguéraud, Characteristic formulae for the verification of imperative programs, 2013. Unpublished

A. Charguéraud, The CFML tool and library, 2016.

M. Clochard, J. Filliâtre, and A. Paskevich, How to Avoid Proving the Absence of Integer Overflows, Verified Software: Theories, Tools and Experiments, pp.94-109, 2015.
DOI : 10.1007/978-3-642-38574-2_1
URL : https://hal.archives-ouvertes.fr/hal-01162661

J. Esparza, P. Lammich, R. Neumann, T. Nipkow, A. Schimpf et al., A Fully Verified Executable LTL Model Checker, Computer Aided Verification (CAV), pp.463-478, 2013.
DOI : 10.1007/978-3-642-39799-8_31
URL : https://hal.archives-ouvertes.fr/hal-01226469

J. Filliâtre, Backtracking iterators, Proceedings of the 2006 workshop on ML , ML '06, pp.55-62, 2006.
DOI : 10.1145/1159876.1159885

J. Filliâtre and M. Pereira, A Modular Way to Reason About Iteration, NASA Formal Methods (NFM), pp.322-336, 2016.
DOI : 10.1007/978-3-319-40648-0_24

J. Filliâtre and P. Letouzey, Functors for Proofs and Programs, European Symposium on Programming (ESOP), pp.370-384, 2004.
DOI : 10.1007/978-3-540-24725-8_26

R. W. Floyd, Assigning meanings to programs, of Proceedings of Symposia in Applied Mathematics, pp.19-32, 1967.
DOI : 10.1090/psapm/019/0235771

C. Haack and C. Hurlin, Resource Usage Protocols for Iterators., The Journal of Object Technology, vol.8, issue.4, pp.55-83, 2009.
DOI : 10.5381/jot.2009.8.4.a3
URL : https://hal.archives-ouvertes.fr/inria-00410128

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

P. Hudak, J. Hughes, S. P. Jones, and P. Wadler, A history of Haskell, Proceedings of the third ACM SIGPLAN conference on History of programming languages , HOPL III, 2007.
DOI : 10.1145/1238844.1238856

G. Hutton, A tutorial on the universality and expressiveness of fold, Journal of Functional Programming, vol.9, issue.4, pp.355-372, 1999.
DOI : 10.1017/S0956796899003500

]. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, Principles of Programming Languages (POPL), pp.247-259, 2015.
DOI : 10.1145/2775051.2676966
URL : https://hal.archives-ouvertes.fr/hal-01078386

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

R. Neelakantan, J. Krishnaswami, L. Aldrich, K. Birkedal, A. Svendsen et al., Design patterns in separation logic, Types in Language Design and Implementation (TLDI), pp.105-116, 2009.

P. Lammich, Automatic Data Refinement, Interactive Theorem Proving, pp.84-99, 2013.
DOI : 10.1007/978-3-642-39634-2_9

P. Lammich, Refinement to Imperative/HOL, Interactive Theorem Proving, pp.253-269, 2015.
DOI : 10.1007/978-3-319-22102-1_17

P. Lammich, Refinement based verification of imperative data structures, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pp.27-36, 2016.
DOI : 10.1145/2854065.2854067

P. Lammich and A. Lochbihler, The Isabelle Collections Framework, Interactive Theorem Proving, pp.339-354, 2010.
DOI : 10.1007/978-3-642-14052-5_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.167.7243

P. Lammich and R. Meis, A separation logic framework for Imperative HOL. Archive of Formal Proofs, 2012.

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Principles of Programming Languages (POPL), pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

B. Liskov and J. V. Guttag, Program Development in Java ? Abstraction, Specification, and Object-Oriented Design, 2001.

A. Lochbihler, Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable, Interactive Theorem Proving (ITP), pp.116-132, 2013.
DOI : 10.1007/978-3-642-39634-2_11

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal, Abstract Predicates and Mutable ADTs in Hoare Type Theory, European Symposium on Programming (ESOP), pp.189-204, 2007.
DOI : 10.1007/978-3-540-71316-6_14

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: dependent types for imperative programs, International Conference on Functional Programming (ICFP), pp.229-240, 2008.

M. Parkinson and G. Bierman, Separation logic and abstraction, Principles of Programming Languages (POPL), pp.247-258, 2005.
DOI : 10.1145/1040305.1040326
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.5332

N. Polikarpova, J. Tschannen, and C. A. Furia, A Fully Verified Container Library, Formal Methods (FM), pp.13-2016
DOI : 10.1007/978-3-319-19249-9_26

F. Pottier, Self-contained archive. http://gallium. inria.fr/~fpottier, 2016.

G. Ramalingam, A. Varshavsky, J. Field, D. Goyal, and S. Sagiv, Deriving specialized program analyses for certifying component-client conformance, Programming Language Design and Implementation (PLDI), pp.83-94, 2002.
DOI : 10.1145/512529.512540

Y. Régis-gianas and F. Pottier, A Hoare Logic for Call-by-Value Functional Programs, Mathematics of Program Construction (MPC), pp.305-335, 2008.
DOI : 10.1007/978-3-540-70594-9_17

Y. Kiam-tan, M. O. Myreen, R. Kumar, A. C. Fox, S. Owens et al., A new verified compiler backend for CakeML, International Conference on Functional Programming (ICFP), pp.60-73, 2016.