J. Andersson, S. Andersson, K. Boortz, M. Carlsson, H. Nilsson et al., SICStus Prolog User"s Manual, 1993.

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/978-3-642-03359-9_8

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, The Matita Interactive Theorem Prover, pp.978-981, 2011.
DOI : 10.1007/978-3-642-22438-6_7

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions, Logical Methods in Computer Science, vol.8, issue.1, 2012.

K. Baelde, A. Chaudhuri, D. Gacek, G. Miller, A. Nadathur et al., Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, pp.1-89, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

B. Barras, Auto-validation d'un système de preuves avec familles inductives, 1999.

C. Belleanne, P. Brisset, and O. Ridoux, A Pragmatic Reconstruction of Lambda-Prolog, Journal of Logic Programming, 1998.

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher Order Logics, vol.5170, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00331193

M. Boespflug, Q. Carbonneaux, O. Hermant, ;. Avigad, S. Kong et al., Coq development team. The Coq proof assistant reference manual. Inria, 2017. L. de Moura, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, vol.878, pp.28-43, 2012.

L. De-moura, S. Kong, J. Avigad, F. Van-doorn, and J. Von-raumer, The Lean Theorem Prover (System Description), pp.978-981, 2015.

G. J. Duck, P. J. Stuckey, M. G. De-la-banda, and C. Holzbaur, The refined operational semantics of constraint handling rules, Logic Programming, pp.90-104, 2004.

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: fast, Embeddable, ?Prolog Interpreter, Proceedings of LPAR, 2015.

C. Dunchev, E. Sacerdoti-coen, and . Tassi, Implementing HOL in an Higher Order Logic Programming Language, Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '16, vol.4, pp.1-4, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01394686

G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. De-moura, A metaprogramming framework for formal verification, Proc. ACM Program. Lang, vol.1, pp.2475-1421, 2017.

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

A. P. Felty and D. Miller, Encoding a dependent-type lambda-calculus in a logic programming language, Proceedings of the 10th International Conference on Automated Deduction, pp.221-235, 1990.

H. Geuvers and G. I. Jojgov, Open Proofs and Open Terms: A Basis for Interactive Logic, Computer Science Logic, 16th International Workshop, p.11, 2002.

, Annual Conference of the EACSL, pp.537-552, 2002.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP, vol.7998, pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

H. Herbelin, Type inference with algebraic universes in the Calculus of Inductive Constructions, 2005.

T. Libal and D. Miller, Functions-as-constructors Higher-order Unification, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), pp.1-17, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01379683

Z. Luo, ECC, an Extended Calculus of Constructions, Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), pp.386-395, 1989.

Z. Luo, Coercive Subtyping in Type Theory, Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, pp.276-296, 1996.

Z. Luo, S. Soloviev, and T. Xue, Coercive subtyping: Theory and implementation, Inf. Comput, vol.223, pp.890-5401, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01130574

A. Mahboubi and E. Tassi, Canonical Structures for the working Coq user, ITP 2013, 4th Conference on Interactive Theorem Proving, vol.7998, pp.19-34, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816703

F. Mazzoli and A. Abel, Type checking through unification, 2016.

D. Miller, ;. D. Miller, and G. Nadathur, Unification Under a Mixed Prefix, 3rd Int. Conf. Logic Programming, vol.14, pp.448-462, 1986.

D. Miller and G. Nadathur, Programming with Higher-Order Logic, p.9780521879408, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, 1991.

U. , Dependently Typed Programming in Agda, Proceedings of the 6th International Conference on Advanced Functional Programming, AFP'08, pp.230-266

. Springer-verlag, , pp.978-981, 2009.

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitationàbilitationà diriger les recherches, 1996.

X. Qi, A. Gacek, S. Holte, G. Nadathur, and Z. Snow, The Teyjus System-Version 2, 2015.

F. Rabe, The MMT API: A Generic MKM System, Intelligent Computer Mathematics, pp.339-343, 2013.

M. R. Blanco and Z. Chihani, Translating between implicit and explicit versions of proof, CADE-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01645016

S. Coen and E. Tassi, Nonuniform Coercions via Unification Hints, TYPES, pp.16-29, 2009.

Z. Snow, D. Baelde, and G. Nadathur, A meta-programming approach to realizing dependently typed logic programming, Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP '10, pp.187-198, 2010.

B. Werner, Une Théorie des Constructions Inductives, 1994.

J. Wielemaker, T. Schrijvers, M. Triska, T. Lager, and . Swi-prolog, Theory and Practice of Logic Programming, vol.12, issue.1-2, pp.67-96, 2012.