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, CAS- SIS, 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.9589

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.
DOI : 10.1007/978-3-642-17164-2_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.461.4140

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.431.9140

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
URL : https://pure.itu.dk/ws/files/32319626/story.pdf

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