Y. An, J. Janssen, and E. Milios, Characterizing and Mining the Citation Graph of the Computer Science Literature, Knowledge and Information Systems, vol.393, issue.6, pp.664-678, 2004.
DOI : 10.1007/s10115-003-0128-3

J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.27, issue.4
DOI : 10.1007/s10817-015-9335-3
URL : https://hal.archives-ouvertes.fr/hal-01211748

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Automated Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban, A learning-based relevance filter for Isabelle

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, International Joint Conference on Automated Reasoning, pp.107-121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, The TLA???+??? Proof System: Building a Heterogeneous Verification Platform, International Colloquium on Theoretical Aspects of Computing, p.44, 2010.
DOI : 10.1007/978-3-642-14808-8_3
URL : https://hal.archives-ouvertes.fr/inria-00521886

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

M. E. Crovella and A. Bestavros, Self-similarity in World Wide Web traffic: evidence and possible causes, IEEE/ACM Transactions on Networking, vol.5, issue.6, pp.835-846, 1997.
DOI : 10.1109/90.650143

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in Isabelle/HOL, Interactive Theorem Proving, pp.279-294, 2013.

C. Kaliszyk and J. Urban, HOL(y)Hammer: Online ATP Service for HOL Light, Mathematics in Computer Science, vol.50, issue.1, pp.5-22, 2015.
DOI : 10.1007/s11786-014-0182-0

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

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

A. Lochbihler, Java and the Java Memory Model ??? A Unified, Machine-Checked Formalisation, European Symposium on Programming (ESOP 2012), pp.497-517, 2012.
DOI : 10.1007/978-3-642-28869-2_25

D. Matichuk, T. Murray, J. Andronick, R. Jeffery, G. Klein et al., Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification, 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, 2015.
DOI : 10.1109/ICSE.2015.85

R. Matuszewski and P. Rudnicki, Mizar: The first 30 years, Mechanized Mathematics and Its Applications, pp.3-24, 2005.

J. Meng and L. C. Paulson, Lightweight relevance filtering for machine-generated resolution problems, Journal of Applied Logic, vol.7, issue.1, pp.41-57, 2009.
DOI : 10.1016/j.jal.2007.07.004

T. Nipkow and G. Klein, Concrete Semantics with Isabelle, 2014.

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL?A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, International Workshop on the Implementation of Logics, pp.1-11, 2010.

A. Riazanov and A. Voronkov, The design and implementation of Vampire, pp.91-110, 2002.

S. Schulz, System Description: E??1.8, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), pp.735-743, 2013.
DOI : 10.1007/978-3-642-45221-5_49

M. Staples, R. Jeffery, J. Andronick, T. Murray, G. Klein et al., Productivity for proof engineering, Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, ESEM '14, pp.1-15, 2014.
DOI : 10.1145/2652524.2652551

J. Urban, MPTP 0.2: Design, Implementation, and Initial Experiments, Journal of Automated Reasoning, vol.15, issue.1, pp.21-43, 2006.
DOI : 10.1007/s10817-006-9032-3

J. Urban, P. Rudnicki, and G. Sutcliffe, ATP and Presentation Service for Mizar Formalizations, Journal of Automated Reasoning, vol.2, issue.2, pp.229-241, 2013.
DOI : 10.1007/s10817-012-9269-y

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, Conference on Automated Deduction (CADE- 22), pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38

M. Wenzel, Isabelle/Isar?A Versatile Environment for Human-Readable Formal Proof Documents, 2002.

F. Wiedijk, Statistics on digital libraries of mathematics. Studies in Logic, Grammar and Rhetoric, 2009.