B. Accattoli, P. Barenbaum, and D. Mazza, Distilling abstract machines, Proceedings of the 19th International conference on Functional programming, pp.363-376, 2014.
DOI : 10.1145/2692915.2628154

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

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, p.2012
DOI : 10.2168/LMCS-8(1:18)2012

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

Y. Bertot and G. Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical Big Operators, Theorem Proving in Higher Order Logics, 2008.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The lambda-Pi-calculus Modulo as a Universal Proof Language, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving CEUR Workshop Proceedings, pp.28-43, 2012.

J. Cheney, The Complexity of Equivariant Unification, pp.332-344, 2004.
DOI : 10.1007/978-3-540-27836-8_30

C. Sacerdoti-coen and E. Tassi, Nonuniform Coercions via Unification Hints, TYPES, pp.16-29, 2009.
DOI : 10.4204/EPTCS.53.2

L. Mendonça-de-moura, J. Avigad, S. Kong, and C. Roux, Elaboration in Dependent Type Theory, 1505.

C. Dunchev, C. Sacerdoti-coen, and E. 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, pp.1-410, 2016.
DOI : 10.1145/2966268.2966272
URL : https://hal.archives-ouvertes.fr/hal-01394686

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter, Proceedings of LPAR, 2015.
DOI : 10.1007/978-3-662-48899-7_32

T. Frhwirth, Constraint Handling Rules, 2009.

A. Gacek, The Abella Interactive Theorem Prover (System Description), Proceedings of IJCAR 2008, pp.154-161, 2008.
DOI : 10.1007/978-3-540-71070-7_13

A. Gacek, D. Miller, and G. Nadathur, Nominal abstraction. Information and Computation, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004
URL : http://doi.org/10.1016/j.ic.2010.09.004

H. Geuvers and G. I. Jojgov, Open Proofs and Open Terms: A Basis for Interactive Logic In Computer Science Logic, 16th International Workshop, CSL, 11th Annual Conference of the EACSL Proceedings, 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, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

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

J. Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, vol.6, issue.3, pp.199-207, 2007.
DOI : 10.1007/s10990-007-9018-9
URL : https://hal.archives-ouvertes.fr/hal-00154508

Z. Luo and . Ecc, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.386-395, 1989.
DOI : 10.1109/LICS.1989.39193
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7596

Z. Luo, Coercive subtyping in type theory, Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, pp.276-296, 1996.
DOI : 10.1007/3-540-63172-0_45

F. Mazzoli and A. Abel, Type checking throug unification. CoRR, abs, 1609.

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, pp.253-281, 1991.
DOI : 10.1007/bfb0038698
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.160.8728

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 and G. Nadathur, Higher-order logic programming, 3rd Int. Conf. Logic Programming, pp.448-462, 1986.
DOI : 10.1007/3-540-16492-8_94
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
DOI : 10.1017/cbo9781139021326
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, issue.1-2, p.51, 1991.
DOI : 10.1016/0168-0072(91)90068-W
URL : http://doi.org/10.1016/0168-0072(91)90068-w

U. Norell, Dependently Typed Programming in Agda, Proceedings of the 6th International Conference on Advanced Functional Programming, AFP'08, pp.230-266, 2009.
DOI : 10.1145/1481861.1481862

F. Rabe, The MMT API: A Generic MKM System, pp.339-343, 2013.
DOI : 10.1007/978-3-642-39320-4_25
URL : http://arxiv.org/abs/1306.3199

N. Zhou, The Language Features and Architecture of B-prolog. Theory Pract, Log. Program, vol.12, issue.12, pp.189-218, 2012.