D. Aspinall, Proof General: A Generic Tool for Proof Development, TACAS, volume 1785 of LNCS, pp.38-42, 2000.
DOI : 10.1007/3-540-46419-0_3

D. Aspinall, C. Lüth, and D. Winterstein, A Framework for Interactive Proof, Calculemus/MKM, pp.161-175, 2007.
DOI : 10.1007/978-3-540-73086-6_15

M. Barnett, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, CASSIS, pp.49-69, 2005.
DOI : 10.1007/978-3-540-30569-9_3

B. Barras, C. Tankink, and E. Tassi, Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface, Proceedings of ITP, 2015.
DOI : 10.1007/978-3-319-22102-1_4
URL : https://hal.archives-ouvertes.fr/hal-01135919

J. Bengtson, J. B. Jensen, F. Sieczkowski, and L. Birkedal, Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq, Lecture Notes in Computer Science, vol.218, pp.22-38, 2011.
DOI : 10.1016/j.entcs.2008.10.022

S. Boldo, J. Jourdan, X. Leroy, and G. Melquiond, A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.107-115, 2013.
DOI : 10.1109/ARITH.2013.30
URL : https://hal.archives-ouvertes.fr/hal-00743090

J. Charles and J. R. Kiniry, A Lightweight Theorem Prover Interface for Eclipse, UITP Workshop proceedings, 2008.

E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns ? Elements of Reusable Object-Oriented Software, 1994.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

C. Thomas and . Hales, Dense Sphere Packings -a blueprint for formal proofs, 2012.

J. Harrison, . Hol, and . Light, Overview, Theorem Proving in Higher Order Logics, 22nd International Conference Proceedings, pp.60-66, 2009.
DOI : 10.1007/978-1-4302-0821-1_1
URL : https://hal.archives-ouvertes.fr/in2p3-00803620

B. Jacobs and F. Piessens, The VeriFast program verifier, CW Reports, vol.520, 2008.

G. Klein, J. Andronick, K. Elphinstone, T. C. Murray, T. Sewell et al., Comprehensive formal verification of an OS microkernel, ACM Transactions on Computer Systems, vol.32, issue.1, 2014.
DOI : 10.1145/2560537

K. Rustan and M. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, LPAR-16, pp.348-370, 2010.

L. Magnusson and B. Nordström, The Alf proof editor and its proof engine, Types for proofs and programs, pp.213-237, 1994.
DOI : 10.1007/3-540-58085-9_78

H. Mehnert and . Kopitiam, Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code, NASA Formal Methods -Third International Symposium, NFM 2011 Proceedings, pp.518-524, 2011.
DOI : 10.1007/978-3-540-87873-5_10

U. Norell, Towards a practical programming language based on dependent type theory, pp.412-96, 2007.

M. Ring and C. Lüth, Collaborative Interactive Theorem Proving with Clide, ITP, pp.467-482, 2014.
DOI : 10.1007/978-3-319-08970-6_30

A. Velykis, /. Isabelle, and . Eclipse, Software, available on http

M. Wenzel, Asynchronous User Interaction and Tool Integration in Isabelle/PIDE, ITP, pp.515-530, 2014.
DOI : 10.1007/978-3-319-08970-6_33

M. Wenzel, System description: Isabelle/jEdit in 2014, UITP, 2014.
DOI : 10.4204/EPTCS.167.10