A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, Hints in Unification, TPHOLs, pp.84-98, 2009.
DOI : 10.1007/BFb0028402

N. G. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Selected Papers on Automath, pp.375-388, 1994.

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

G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer, How to make ad hoc proof automation less ad hoc, Journal of Functional Programming, vol.23, issue.04, pp.357-401, 2013.
DOI : 10.1017/S0956796813000051
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.3332

F. Guidi, The formal system ????, ACM Transactions on Computational Logic, vol.11, issue.1, pp.1-5, 2009.
DOI : 10.1145/1614431.1614436

F. Guidi, A Verified Translation of Landau's Grundlagen " from Automath into a Pure Type System, via ??, 2015

C. Liang, G. Nadathur, and X. Qi, Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts, Journal of Automated Reasoning, vol.198, issue.1?2, pp.89-132, 2004.
DOI : 10.1007/s10817-004-6885-1

D. Miller, A logic programming language with lambda-abstraction, function variables , and simple unification, Journal of Logic and Computation, vol.1, pp.253-281, 1991.

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

G. Nadathur and D. J. Mitchell, Teyjus -A compiler and abstract machine based implementation of ?prolog, CADE-16, pp.287-291, 1999.

O. Ridoux, Lambda-Prolog de A a Z... ou presque. HabilitationàHabilitation`Habilitationà diriger des recherches, 1998.

M. Sozeau and N. Oury, First-Class Type Classes, TPHOLs, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

L. S. Van-benthem and . Jutting, Checking Landau's " Grundlagen " in the automath system, Mathematical Centre Tracts, vol.83, 1979.