J. Avigad, E. Dean, and J. Mumma, A Formal System for Euclid's Elements. The Review of Symbolic Logic, 2009.

H. Barendregt and F. Wiedijk, The challenge of computer mathematics, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.42, issue.1835, pp.2351-2375, 1835.
DOI : 10.1098/rsta.2005.1650

M. Bezem and T. Coquand, Automating Coherent Logic, 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ? LPAR 2005, 2005.
DOI : 10.1007/11591191_18

M. Bezem and D. Hendriks, On the Mechanization of the Proof of Hessenberg???s Theorem in Coherent Logic, Journal of Automated Reasoning, vol.19, issue.1, 2008.
DOI : 10.1007/s10817-007-9086-x

C. Jasmin and . Blanchette, Redirecting Proofs by Contradiction, Third International Workshop on Proof Exchange for Theorem Proving, pp.11-26, 2013.

J. Christian-blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Journal of Automated Reasoning, vol.13, issue.5, pp.109-128, 2013.
DOI : 10.1007/s10817-013-9278-5

J. Christian-blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, 8th International Symposium, Proceedings, pp.12-27, 2011.
DOI : 10.1007/BFb0028402

A. Blass, TOPOI AND COMPUTATION, Bulletin of the EATCS, vol.36, pp.57-65, 1998.
DOI : 10.1142/9789812794499_0023

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus Modulo as a Universal Proof Language, Second Workshop on Proof Exchange for Theorem Proving (PxTP) CEUR Workshop Proceedings, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

N. Govert-de-bruijn, The Mathematical Vernacular, a Language for Mathematics with Typed Sets, Proceedings of the Workshop on Programming Languages, 1987.

J. Fisher and M. Bezem, Skolem Machines and Geometric Logic, 4th International Colloquium on Theoretical Aspects of Computing ? ICTAC 2007, 2007.
DOI : 10.1007/978-3-540-75292-9_14

M. Ganesalingam and W. T. Gowers, A fully automatic problem solver with human-style output. CoRR, abs, 1309.

C. Kaliszyk and A. Krauss, Scalable LCF-Style Proof Translation, Interactive Theorem Proving -4th International Conference, ITP 2013 Proceedings, pp.51-66, 2013.
DOI : 10.1007/978-3-642-39634-2_7

C. Kaliszyk and J. Urban, PRocH: Proof Reconstruction for HOL Light, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, pp.267-274, 2013.
DOI : 10.1007/978-3-642-38574-2_18

C. Keller and B. Werner, Importing HOL Light into Coq, ITP, pp.307-322, 2010.
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604

M. Kohlhase, An OMDoc Primer, Lecture Notes in Computer Science, vol.4180, issue.2, pp.33-34, 2006.
DOI : 10.1007/11826095_5

D. Lee and W. W. Chu, Comparative analysis of six XML schema languages, ACM SIGMOD Record, vol.29, issue.3, pp.76-87, 2000.
DOI : 10.1145/362084.362140

S. Obua and S. Skalberg, Importing HOL into Isabelle/HOL, Automated Reasoning, pp.298-302, 2006.
DOI : 10.1007/11814771_27

A. Polonsky, Proofs, Types and Lambda Calculus, 2011.

P. Rudnicki, Obvious inferences, Journal of Automated Reasoning, vol.3, issue.4, pp.383-393, 1987.
DOI : 10.1007/BF00247436

W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.
DOI : 10.1007/978-3-642-69418-9

S. Smolka and J. C. Blanchette, Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs, Third International Workshop on Proof Exchange for Theorem Proving, pp.117-132, 2013.

S. Stojanovi´cstojanovi´c, J. Narboux, and P. Jani?i´jani?i´c, Synergy Between Interactive and Automated Theorem Proving in Formalization of Mathematical Knowledge: A Case Study of Tarski's Geometry, 2014.

S. Stojanovi´cstojanovi´c, V. Pavlovi´cpavlovi´c, and P. Jani?i´jani?i´c, A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

A. Tarski and S. Givant, Tarski's system of geometry. The Bulletin of Symbolic Logic, 1999.

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, Theorem Proving in Higher Order Logics (TPHOLs'99), pp.167-184, 1999.
DOI : 10.1007/3-540-48256-3_12

F. Wiedijk, Mathematical Vernacular Unpublished note, 2000.

F. Wiedijk, A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving, Logical Methods in Computer Science, vol.8, issue.1, p.2012
DOI : 10.2168/LMCS-8(1:30)2012