Abel, A., Pientka, B.: Higher-order dynamic pattern unification for dependent types and records. In: Typed Lambda Calculi and Applications, pp 10–26. Springer (2011)
Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a Proof Assistant. In: Types for Proofs and Programs, pp 18–32. Springer (2006)
Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: Hints in Unification. In: International Conference on Theorem Proving in Higher Order Logics, pp 84–98. Springer, Berlin (2009)
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: A system for reasoning about relational specifications. J. of Formalized Reasoning (2014)
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, Volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier, New York (1984)
Benzmüller, C., Kohlhase, M.: LEO – a Higher Order Theorem Prover. In: 15Th Conf. on Automated Deduction (CADE), pp 139–144 (1998)
Benzmüller, C., Kohlhase, M.: LEO – a Higher Order Theorem Prover. In: 15Th Conf. on Automated Deduction (CADE), pp 139–144 (1998)
Bove, A., Dybjer, P., Norell, U.: A Brief Overview of Agda - A Functional Language with Dependent Types. In: TPHOLs, vol. 5674, pp 73–78. Springer (2009)
Fettig, R., Löchner, B.: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In: RTA 1996, LNCS, pp 347–361 (1103)
Goldfarb, W.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225–230 (1981) DOI: 10.1016/0304-3975(81)90040-2
Guidi, F., Coen, C.S., Tassi, E.: Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29.8, 1125–1150 (2019) DOI: 10.1017/S0960129518000427
Hamana, M.: How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. In: Proceedings of the ACM on Programming Languages 1.ICFP, pp 1–28 (2017)
Makoto, H.: A functional implementation of function-as-constructor higher-order unification. In: Proc. 31st International Workshop on Unification (UNIF’17) (2017)
Hamana, M., Abe, T., Murase, Y., Sakaguchi, K.: The System SOL: Second-Order Laboratory. In: 6th International Workshop on Confluence (2020)
Huet, G.: The undecidability of unification in third order logic. Inf. Control. 22, 257–267 (1973) DOI: 10.1016/S0019-9958(73)90301-X
Huet, G.: A unification algorithm for typed λ-calculus. Theor. Comput. Sci. 1, 27–57 (1975) DOI: 10.1016/0304-3975(75)90011-0
Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11, 31–55 (1978) DOI: 10.1007/BF00264598
Libal, T., Miller, D.: Functions-as-constructors higher-order unification. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (2016)
McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic 3(1), 80–136 (2002) DOI: 10.1145/504077.504080
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation 1(4), 497–536 (1991) DOI: 10.1093/logcom/1.4.497
Miller, D., Nadathur, G.: Some uses of higher-order logic in computational linguistics. In: Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pp 247–255 (1986)
Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14 (4), 321–358 (1992) DOI: 10.1016/0747-7171(92)90011-R
Miller, D., Nadathur, G.: Programming with Higher-Order logic. Cambridge University Press, Cambridge (2012) DOI: 10.1017/CBO9781139021326
Nadathur, G., Mitchell, D.J.: System description: Teyjus – A compiler and abstract machine based implementation of λ prolog. CADE 16, LNAI 1632, 287–291 (1999)
Nipkow, T.: Functional unification of higher-order patterns. In: Vardi, M. (ed.) 8th Symp. on Logic in Computer Science, pp 64–74. IEEE (1993)
Nipkow, T., Paulson, L.C., Markus, W.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, Berlin (2002)
Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Kahn, G. (ed.) 6th Symp. on Logic in Computer Science, pp 74–85. IEEE (1991)
Pfenning, F., Schürmann, C.: System description: Twelf – A meta-logical framework for deductive systems. CADE 16, LNAI 1632, pp. 202–206 Trento (1999)
Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR, LNCS, vol. 6173, pp 15–21 (2010)
Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system – version 2. http://teyjus.cs.umn.edu/ (2015)
Schwichtenberg, H.: Minlog. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, volume 3600 of LNCS, pp 151–157. Springer (2006)
Snyder, W., Gallier, J.H.: Higher order unification revisited: Complete sets of transformations. J. Symb. Comput. 8(1-2), 101–140 (1989) DOI: 10.1016/S0747-7171(89)80023-9
Tassi, E.: Private communication (Unknown Month 2016)
Tiu, A.F.: An extension of L-lambda unification http://www.ntu.edu.sg/home/atiu/llambdaext.pdf (2002)
Qian, Z.: Linear Unification of Higher-Order Patterns. Proc. Coll. Trees in Algebra and Programming (1993)
Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2020)
Tetsuo, Y., Hu, Z., Takeichi, M.: Deterministic Higher-Order patterns for program transformation international symposium on Logic-Based program synthesis and transformation. Springer, Berlin (2004)
Tetsuo, Y., Hu, Z., Takeichi, M.: Deterministic second-order patterns for program transformation. Comput. Softw. 21(5), 71–76 (2004). In Japanese
Ziliani, B., Sozeau, M.: A unification algorithm for Coq featuring universe polymorphism and overloading. ICFP, 179–191 (2015)
