Decidability of bounded higher-order unification

Andrews, 1986 Andrews, 2001, Classical type theory, vol. 2, 965 Barendregt, 1984 Barendregt, 1990, Functional programming and lambda calculus, vol. B, 321 Beckmann, 2001, Exact bounds for lengths of reductions in typed λ-calculus, J. Symbolic Logic, 66, 1277, 10.2307/2695106 Bird, 1998 Burstall, R., MacQueen, D., Sanella, D.T., 1980. Hope: an experimental applicative language. In: Proc. LISP Conference. pp. 136–143 Baader, 1994, Unification theory, 41 Comon, 1997, Higher-order matching and tree automata, vol. 1414, 157 Comon, 1998, Completion of rewrite systems with membership constraints. Part I: Deduction rules, J. Symbolic Comput., 25, 397, 10.1006/jsco.1997.0185 Cervesato, 1997, Linear higher-order pre-unification, 422 Dershowitz, 1990, Rewrite systems, vol. B, 243 Dowek, 1992, Third order matching is decidable, 2 Dowek, 1994, Third order matching is decidable, Ann. Pure Appl. Logic, 69, 135, 10.1016/0168-0072(94)90083-3 Dowek, 2001, Higher-order unification and matching, vol. 2, 1009 Dougherty, 2002, A decidable variant of higher order matching, vol. 2378, 340 Farmer, 1988, A unification algorithm for second order monadic terms, Ann. Pure Appl. Logic, 39, 131, 10.1016/0168-0072(88)90015-2 Farmer, 1991, Simple second-order languages for which unification is undecidable, J. Theoret. Comput. Sci., 87, 173, 10.1016/S0304-3975(06)80003-4 Gandy, 1980, Proofs of strong normalization, 457 Goubault-Larrecq, 1997, Proof Theory and Automated Deduction, vol. 6 Goldfarb, 1981, The undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225, 10.1016/0304-3975(81)90040-2 Gutierrez, 1998, Satisfiability of word equations with constants is in exponential space, 112 Hindley, 1997, Basic Simple Type Theory, 10.1017/CBO9780511608865 Hanus, 1995, Curry: A truly functional logic language, 95 Hindley, 1986 Huet, 1975, A unification algorithm for typed λ-calculus, Theoret. Comput. Sci., 1, 27, 10.1016/0304-3975(75)90011-0 Huet, G., 1976. Résolution d’équations dans des langages d’ordre 1,2,…ω. Thèse de doctorat d‘etat, Université Paris VII (in French) Jensen, 1976, Mechanizing ω-order type theory through unification, Theoret. Comput. Sci., 3, 123, 10.1016/0304-3975(76)90021-9 Klop, 1992, Term rewriting systems, vol. 2, 2 Kościelski, 1996, Complexity of Makanin’s algorithms, J. Assoc. Comput. Machinery, 43, 670, 10.1145/234533.234543 Levy, 1996, Linear second order unification, vol. 1103, 332 Loader, 2003, Higher order beta matching is undecidable, Logic J. IGPL, 11, 51, 10.1093/jigpal/11.1.51 Levy, 2000, On the undecidability of second-order unification, Inform. and Comput., 159, 125, 10.1006/inco.2000.2877 Levy, 2000, Linear second-order unification and context unification with tree-regular constraints, vol. 1833, 156 Makanin, 1977, The problem of solvability of equations in a free semigroup, Math. USSR Sbornik, 32, 129, 10.1070/SM1977v032n02ABEH002376 Miller, 1991, A logic programming language with lambda-abstraction, function variables and simple unification, J. Logic Comput., 1, 497, 10.1093/logcom/1.4.497 Narendran, P., 1990. Some remarks on second order unification. Technical Report, Inst. of Programming and Logics, Department of Computer Science, Univ. of NY at Albany Nipkow, T., 1991. Higher-order critical pairs, Proc. 6th IEEE Symp. LICS, pp. 342–349 Niehren, 1997, On equality up-to constraints over finite trees, context unification, and one-step rewriting, vol. 1249, 34 Niehren, 2000, On rewrite constraints and context unification, Inform. Process. Lett., 74, 35, 10.1016/S0020-0190(00)00036-3 Padovani, 2000, Decidability of fourth-order matching, Math. Structures Comput. Sci., 10, 361, 10.1017/S0960129500003108 Paulson, 1991 Paulson, 1994, Isabelle, vol. 828 Pfenning, 2001, Logical frameworks, vol. 2, 1063 Plandowski, 1999, Satisfiability of word equations with constants is in PSPACE, 495 Schwichtenberg, 1982, Complexity of normalization in the pure typed λ-calculus, vol. 110, 453 Schulz, 1990, Makanin’s algorithm — two improvements and a generalization, vol. 572, 85 Schwichtenberg, 1991, An upper bound for reduction sequences in the typed λ-calculus, Arch. Math. Logic, 30, 405, 10.1007/BF01621476 Schulz, 1993, Word unification and transformation of generalized equations, J. Automat. Reason., 149, 10.1007/BF00881904 Schmidt-Schauß, M., 1994. Unification of stratified second-order terms. Internal Report 12/94, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt, Frankfurt, Germany Schmidt-Schauß, 1999 Schmidt-Schauß, 1999 Schmidt-Schauß, 2001, Stratified context unification is in PSPACE, vol. 2142, 498 Schmidt-Schauß, 2002, A decision algorithm for stratified context unification, J. Logic Comput., 12, 929, 10.1093/logcom/12.6.929 Schmidt-Schauß, 2003, Decidability of arity-bounded higher-order matching, 2741, 488 Schmidt-Schauß, 2004, Decidability of bounded second order unification, Inform. and Comput., 188, 143, 10.1016/j.ic.2003.08.002 Schmidt-Schauß, 1998, On the exponent of periodicity of minimal solutions of context equations, vol. 1379, 61 Schmidt-Schauß, 2002, Decidability of bounded higher-order unification, vol. 2471, 522 Schmidt-Schauß, 2002, Solvability of context equations with two context variables is decidable, J. Symbolic Comput., 33, 77, 10.1006/jsco.2001.0438 Statman, 1979, The typed λ-calculus is not elementary recursive, Theoret. Comput. Sci., 9, 73, 10.1016/0304-3975(79)90007-0 Turner, 1985, Miranda: A non-strict functional language with polymorphic types, vol. 201, 1 Vorobyov, 1998, ∀∃∗-equational theory of context unification is Π10-hard, vol. 1450, 597 Wierzbicki, 1999, Complexity of the higher-order matching, vol. 1632, 82 Wolfram, 1993, The Clausal Theory of Types, vol. 21 Zhezherun, 1979, Decidability of the unification problem for second order languages with unary function symbols, Kibernetika (Kiev), 5, 120