A. Abel and B. Pientka, Higher-Order Dynamic Pattern Unification for Dependent Types and Records, Typed Lambda Calculi and Applications, pp.10-26, 2011.
DOI : 10.1007/978-3-642-14203-1_2

B. Andrews, F. Pfenning, S. Issar, and C. P. Klapper, The TPS theorem proving system, LNCS, vol.8, issue.230, pp.663-664, 1986.

C. Asperti, E. Sacerdoti-coen, S. Tassi, and . Zacchiroli, Crafting a Proof Assistant, Types for Proofs and Programs, pp.18-32, 2006.
DOI : 10.1007/978-3-540-74464-1_2

K. Baelde, A. Chaudhuri, D. Gacek, G. Miller, A. Nadathur et al., Abella: A system for reasoning about relational specifications, J. of Formalized Reasoning, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984.

C. Benzmüller, F. Rabe, and G. Sutcliffe, THF0 ??? The Core of the TPTP Language for Higher-Order Logic, Automated Reasoning, pp.491-506, 2008.
DOI : 10.1007/978-3-540-71070-7_41

A. Bove, P. Dybjer, and U. Norell, A Brief Overview of Agda ??? A Functional Language with Dependent Types, TPHOLs, pp.73-78, 2009.
DOI : 10.1007/978-3-540-87827-8_28

E. Chad and . Brown, Satallax: An automatic higher-order prover, Automated Reasoning, pp.111-117, 2012.

. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, 1940.
DOI : 10.2307/2371199

M. Dalrymple, S. M. Shieber, and F. C. Pereira, Ellipsis and higher-order unification, Linguistics and Philosophy, vol.8, issue.1, pp.399-452, 1991.
DOI : 10.1007/BF00630923

D. Duggan, Unification with extended patterns, Theoretical Computer Science, vol.206, issue.1-2, pp.1-50, 1998.
DOI : 10.1016/S0304-3975(97)00141-2

B. Fettig and . Löchner, Unification of higher-order patterns in a simply typed lambdacalculus with finite products and terminal type, RTA 1996, pp.347-361

W. Goldfarb, The undecidability of the second-order unification problem, Theoretical Computer Science, vol.13, issue.2, pp.225-230, 1981.
DOI : 10.1016/0304-3975(81)90040-2

G. Huet, The undecidability of unification in third order logic, Information and Control, vol.22, issue.3, pp.257-267, 1973.
DOI : 10.1016/S0019-9958(73)90301-X

G. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

G. Huet and B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica, vol.11, issue.1, pp.31-55, 1978.
DOI : 10.1007/BF00264598

R. Mcdowell and D. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002.
DOI : 10.1145/504077.504080

. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

D. Miller and G. Nadathur, Some uses of higher-order logic in computational linguistics, Proceedings of the 24th annual meeting on Association for Computational Linguistics -, pp.247-255, 1986.
DOI : 10.3115/981131.981165

. 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

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

G. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, CADE, vol.16, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

T. Nipkow, Functional unification of higher-order patterns, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.64-74, 1993.
DOI : 10.1109/LICS.1993.287599

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, Number 2283 in LNCS, 2002.

F. Pfenning, Unification and anti-unification in the Calculus of Constructions 28 Frank Pfenning and Carsten Schürmann. System description: Twelf ? A meta-logical framework for deductive systems, 6th Symp. on Logic in Computer Science LNAI 1632, pp.74-85, 1991.

B. Pientka and J. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), IJCAR, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2

A. Qi, S. Gacek, G. Holte, Z. Nadathur, and . Snow, The Teyjus system ? version 2, 2015.

H. Schwichtenberg and . Minlog, The Seventeen Provers of the World, LNCS, vol.3600, pp.151-157, 2006.

W. Snyder and J. H. Gallier, Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation, vol.8, issue.1-2, pp.101-140, 1989.
DOI : 10.1016/S0747-7171(89)80023-9

F. Alwen and . Tiu, An extension of L-lambda unification, 2002.

Z. Qian, Linear unification of higher-order patterns, Proc. Coll. Trees in Algebra and Programming, 1993.
DOI : 10.1007/3-540-56610-4_78

M. Wisniewski, A. Steen, and C. Benzmüller, The Leo-III project, Joint Automated Reasoning Workshop and Deduktionstreffen, p.38, 2014.

B. Ziliani and M. Sozeau, A unification algorithm for Coq featuring universe polymorphism and overloading, pp.179-191, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01248804