A. W. Appel and A. P. Felty, Lightweight Lemmas in lambda-Prolog, Logic Programming: The 1999 International Conference, pp.411-425, 1999.

R. Arthan, On Definitions of Constants and Types in HOL, Journal of Automated Reasoning, vol.26, issue.2, pp.205-219, 2016.
DOI : 10.1007/s10817-016-9366-4

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, Hints in Unification, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.84-98, 2009.
DOI : 10.1007/BFb0028402

P. Baillot and M. Hofmann, Type inference in intuitionistic linear logic, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.219-230, 2010.
DOI : 10.1145/1836089.1836118
URL : https://hal.archives-ouvertes.fr/hal-00543120

R. Blanco, Z. Chihani, and D. Miller, Translating between implicit and explicit versions of proof

Z. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, Lake Placid Proceedings, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

N. G. De-bruijn, Lambda calculus with namefree formulas in involving symbols that represent reference transforming mappings, Indagationes Mathematicae, pp.348-356, 1978.

D. Delahaye, A Tactic Language for the System Coq, Logic for Programming and Automated Reasoning: 7th International Conference, pp.85-95, 2000.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter, Logic for Programming, Artificial Intelligence and Reasoning: 20th International Conference, pp.460-468, 2015.
DOI : 10.1007/978-3-662-48899-7_32

A. P. Felty, Implementing tactics and tacticals in a higher-order logic programming language, Journal of Automated Reasoning, vol.5, issue.3, pp.41-81, 1993.
DOI : 10.1007/BF00881900

A. P. Felty and D. Miller, Specifying theorem provers in a higher-order logic programming language, 9th International Conference on Automated Deduction Proceedings, pp.61-80, 1988.
DOI : 10.1007/BFb0012823

T. Frhwirth, Theory and practice of constraint handling rules, The Journal of Logic Programming, vol.37, issue.1-3, pp.95-138, 1998.
DOI : 10.1016/S0743-1066(98)10005-5

E. Giachino, E. B. Johnsen, C. Laneve, and K. I. Pun, Time Complexity of Concurrent Programs, 1511.
DOI : 10.1007/978-3-319-28934-2_11
URL : https://hal.archives-ouvertes.fr/hal-01229068

M. J. Gordon and A. M. Pitts, The HOL logic and system of Real-Time Safety Critical Systems, Towards Verified Systems, pp.49-70, 1994.

J. Harrison, HOL Light: An Overview, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

J. Harrison 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

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system release 3.08, Documentation and users manual, Projet Cristal, 2004.

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, Interactive Theorem Proving: 4th International Conference Proceedings, pp.19-34, 2013.
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

D. Miller, Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992.
DOI : 10.1016/0747-7171(92)90011-R

D. Miller, Foundational proof certificates, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, LFMTP '13, pp.150-163, 2014.
DOI : 10.1145/2503887.2503894
URL : https://hal.archives-ouvertes.fr/hal-01239733

G. Nadathur and D. J. Mitchell, System Description: Teyjus -A Compiler and Abstract Machine Based Implementation of lambda-Prolog. In Automated Deduction -CADE-16, 16th International Conference on Automated Deduction Proceedings, pp.287-291, 1999.

G. Nadathur and G. Tong, Realizing Modularity in lambdaProlog, Journal of Functional and Logic Programming, issue.2, 1999.

E. Sacerdoti-coen, S. Tassi, and . Zacchiroli, Tinycals: Step by Step Tacticals, Tinycals: Step by Step Tacticals, pp.125-142, 2007.
DOI : 10.1016/j.entcs.2006.09.026

A. Spiwack, An abstract type for constructing tactics in Coq, Proof Search in Type Theory, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00502500

A. Spiwack, An abstract type for constructing tactics in coq. Unpublished, 2010b. URL http://assert-false
URL : https://hal.archives-ouvertes.fr/inria-00502500

D. Whiteside, L. Aspinall, G. Dixon, and . Grov, Towards Formal Proof Script Refactoring, Intelligent Computer Mathematics -18th Symposium , Calculemus 2011, and 10th International Conference Proceedings, pp.260-275, 2011.
DOI : 10.1007/3-540-48256-3_12

F. Wiedijk, The Seventeen Provers of the World, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence, vol.3600, 2006.
DOI : 10.1007/11542384