A. Baumgartner, T. Kutsia, J. Levy, and M. Villaret, Higher-Order Pattern Anti-Unification in Linear Time, Journal of Automated Reasoning, vol.5, issue.1, pp.293-310, 2017.
DOI : 10.1145/1614431.1614437
URL : http://doi.org/10.1007/s10817-016-9383-3

T. Boy-de-la-tour and N. Peltier, Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization, Journal of Automated Reasoning, vol.137, issue.1???2, pp.245-280, 2016.
DOI : 10.1023/A:1026247421383

N. G. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag Math, vol.34, issue.5, pp.381-392, 1972.

G. Dowek, Higher-Order Unification and Matching, Handbook of Automated Reasoning, pp.1009-1062, 2001.
DOI : 10.1016/B978-044450813-3/50018-7

R. O. Gandy, An early proof of normalization by A.M. Turing, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.453-455, 1980.

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

K. Hirata, T. Ogawa, and M. Harao, Generalization Algorithms for Second-Order Terms, Inductive Logic Programming, 14th International Conference, pp.147-163, 2004.
DOI : 10.1007/978-3-540-30109-7_14
URL : http://www.dumbo.ai.kyutech.ac.jp/hirata/papers/ILP2004-revised.pdf

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
URL : https://doi.org/10.1016/0304-3975(75)90011-0

D. C. Jensen and T. Pietrzykowski, Mechanizing ??-order type theory through unification, Theoretical Computer Science, vol.3, issue.2, pp.123-171, 1976.
DOI : 10.1016/0304-3975(76)90021-9
URL : https://doi.org/10.1016/0304-3975(76)90021-9

J. Lassez, M. Maher, and K. Marriot, Unification revisited, Foundations of Deductive Databases and Logic Programming, pp.67-113, 1988.
DOI : 10.1007/3-540-19129-1_4

T. M. Mitchell, Generalization as search, Artificial Intelligence, vol.18, issue.2, pp.203-226, 1982.
DOI : 10.1016/0004-3702(82)90040-6

F. Pfenning, Unification and anti-unification in the calculus of constructions, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.74-85, 1991.
DOI : 10.1109/LICS.1991.151632

T. Pietrzykowski, A Complete Mechanization of Second-Order Type Theory, Journal of the ACM, vol.20, issue.2, pp.333-364, 1973.
DOI : 10.1145/321752.321764