{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T15:39:14Z","timestamp":1757777954854},"reference-count":143,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50018-7","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1009-1062","source":"Crossref","is-referenced-by-count":45,"title":["Higher-Order Unification and Matching"],"prefix":"10.1016","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/B978-044450813-3\/50018-7_bb0010","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","article-title":"Explicit substitutions","volume":"1","author":"Abadi","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0015","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01621471","article-title":"The undecidability of the second order predicate unification problem","volume":"30","author":"Amiot","year":"1990","journal-title":"Archive for mathematical logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0020","first-page":"965","article-title":"Classical type theory","volume":"Vol. II","author":"Andrews","year":"2001"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50018-7_bb0025","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in type theory","volume":"36","author":"Andrews","year":"1971","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0030","series-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"Andrews","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0035","series-title":"International Conference on Constaints in Computational Logic","first-page":"269","article-title":"Higher-order conditional rewriting and narrowing","author":"Avenhaus","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0040","first-page":"1149","article-title":"Proof-assistants using dependent type systems","volume":"Vol. II","author":"Barendregt","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0045","series-title":"The Lambda-calculus, its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0050","first-page":"118","article-title":"Lambda calculi with types","volume":"Vol. 2","author":"Barendregt","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0055","article-title":"The complexity of unification","author":"Baxter","year":"1977","journal-title":"PhD thesis, University of Waterloo"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50018-7_bb0060","doi-asserted-by":"crossref","first-page":"757","DOI":"10.1017\/S0956796800001969","article-title":"A simple proof of the undecidability of inhabitation in \u03bbP","volume":"6","author":"Bezem","year":"1996","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0065","series-title":"SOFSEM: Theory and Practice of Informatics","first-page":"363","article-title":"Implementation of higher-order unification based on calculus of explicit substitution","author":"Borovansk\u00fd","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0070","series-title":"Principles and Practice of Constraint Programming","first-page":"267","article-title":"AC-unification of higher-order patterns","author":"Boudet","year":"1997"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50018-7_bb0075","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0080","series-title":"Introduction to mathematical logic","author":"Church","year":"1956"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0085","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1006\/jsco.1997.0186","article-title":"Completion of rewrite systems with membership constraints. Part II: Constraint solving","volume":"25","author":"Comon","year":"1998","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0090","series-title":"Conference on Computer Science Logic","first-page":"157","article-title":"Higher-order matching and tree automata","author":"Comon","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0095","article-title":"Une th\u00e9orie des constructions","author":"Coquand","year":"1985","journal-title":"Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0100","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0105","article-title":"Conception d'un langage de haut niveau de repr\u00e9sentation de preuves. r\u00e9currence par filtrage de motifs. unification en pr\u00e9sence de types inductifs primitifs. synth\u00e8se de lemmes d'inversion","author":"Cornes","year":"1997","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50018-7_bb0110","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","article-title":"Confluence properties of weak and strong calculi of explicit substitutions","volume":"43","author":"Curien","year":"1996","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0115","article-title":"Outils pour la preuve par analogie","author":"Curien","year":"1995","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 Henri Poincar\u00e9, Nancy I"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50018-7_bb0120","doi-asserted-by":"crossref","first-page":"49","DOI":"10.2307\/2266302","article-title":"The combinatory foundations of mathematical logic","volume":"7","author":"Curry","year":"1942","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0125","volume":"Vol. 1","author":"Curry","year":"1958"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0130","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BF00630923","article-title":"Ellipsis and higher-order unification","volume":"14","author":"Dalrymple","year":"1991","journal-title":"Linguistic and Philosophy"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0135","series-title":"International Federation for Information Processing Congress","first-page":"67","article-title":"Invited commentary of [Robinson 1969]","author":"Davis","year":"1969"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50018-7_bb0140","doi-asserted-by":"crossref","first-page":"233","DOI":"10.2307\/2318447","article-title":"Hilbert's tenth problem is unsolvable","volume":"80","author":"Davis","year":"1973","journal-title":"The American Mathematician Monthly"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50018-7_bb0145","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0150","series-title":"To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism","article-title":"A survey of the project automath","author":"de Bruijn","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0155","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","article-title":"Higher-order unification via combinators","volume":"114","author":"Dougherty","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0160","series-title":"Conference on Automated Deduction","first-page":"79","article-title":"A combinatory logic approach to higher-order E-unification","author":"Dougherty","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0165","article-title":"D\u00e9monstration automatique dans le calcul des constructions","author":"Dowek","year":"1991","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII"},{"issue":"12","key":"10.1016\/B978-044450813-3\/50018-7_rf0170","first-page":"951","article-title":"L'ind\u00e9cidabilit\u00e9 du filtrage du troisi\u00e8me ordre dans les calculus avec types d\u00e9pendants ou constructeurs de types","volume":"312","author":"Dowek","year":"1991","journal-title":"Comptes Rendus \u00e0 l'Acad\u00e9mie des Sciences I"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0175","first-page":"873","article-title":"L'ind\u00e9cidabilit\u00e9 du filtrage du troisi\u00e8me ordre dans les calculs avec types d\u00e9pendants ou constructeurs de types","volume":"318","author":"Dowek","year":"1991","journal-title":"Comptes Rendus \u00e0 l'Acad\u00e9mie des Sciences I"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0175","series-title":"Mathematical Foundation of Computer Science","first-page":"151","article-title":"A second-order pattern matching algorithm in the cube of typed \u03bb-calculi","author":"Dowek","year":"1991"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50018-7_bb0180","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","article-title":"A complete proof synthesis method for the cube of type systems","volume":"3","author":"Dowek","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0185","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/0304-3975(93)90175-S","article-title":"The undecidability of pattern matching in calculi where primitive recursive functions are representable","volume":"107","author":"Dowek","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0195","series-title":"Typed Lambda Calculi and Applications","first-page":"139","article-title":"The undecidability of typability in the lambda-pi-calculus","author":"Dowek","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0195","series-title":"A unification algorithm for second-order linear terms","author":"Dowek","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0200","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(94)90083-3","article-title":"Third order matching is decidable","volume":"69","author":"Dowek","year":"1994","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0205","series-title":"Typed Lambda Calculi and Applications","first-page":"154","article-title":"Lambda-calculus, combinators and the comprehension scheme","author":"Dowek","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0210","series-title":"Logic in Computer Science","first-page":"366","article-title":"Higher-order unification via explicit substitutions","author":"Dowek","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0215","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500003236","article-title":"HOL-lambda-sigma: an intentional first-order expression of higher-order logic","volume":"11","author":"Dowek","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0220","series-title":"Joint International Conference and Symposium on Logic Programming","first-page":"259","article-title":"Unification via explicit substitutions: the case of higher-order patterns","author":"Dowek","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0225","article-title":"Normal proofs in set theory","author":"Ekman","year":"1994","journal-title":"Doctoral thesis, Chalmers University and University of G\u00f6teborg"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0230","series-title":"International Conference on Rewriting Techniques and Applications","first-page":"121","article-title":"Higher-order unification with dependent function types","author":"Elliott","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0235","article-title":"Extensions and applications of higher-order unification","author":"Elliott","year":"1990","journal-title":"PhD thesis, Carnegie Mellon University"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0240","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","article-title":"A unification algorithm for second-order monadic terms","volume":"39","author":"Farmer","year":"1988","journal-title":"Annals of Pure and applied Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0245","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/S0304-3975(06)80003-4","article-title":"Simple second order languages for which unification is undecidable","volume":"87","author":"Farmer","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0250","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0168-0072(91)90015-E","article-title":"A unification theoretic method for investigating the k-provability problem","volume":"51","author":"Farmer","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0255","series-title":"Logic Colloquium","first-page":"23","article-title":"Equality between functionals","author":"Friedman","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0260","series-title":"Scandinavian Logic Symposium","article-title":"Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types","author":"Girard","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0265","article-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972","journal-title":"Th\u00e8se d'\u00e9tat, Universit\u00e9 de Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0270","series-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0275","doi-asserted-by":"crossref","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","article-title":"\u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes","volume":"12","author":"G\u00f6del","year":"1958","journal-title":"Dialectica"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0280","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0285","series-title":"5th International Conference on Logic Programming and Automated Reasoning","first-page":"129","article-title":"Higher-order rigid E-unification","author":"Goubault","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0290","series-title":"Conference on Automated Deduction","first-page":"588","article-title":"Programming by example and proving by example using higher-order unification","author":"Hagiya","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0295","series-title":"International Conference on Logic Programming","first-page":"270","article-title":"Higher-order unification as a theorem proving procedure","author":"Hagiya","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0300","article-title":"On normalization of proofs in set theory","author":"Halln\u00e4s","year":"1983","journal-title":"Doctoral thesis, University of Stockholm"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0310","series-title":"International Conference and Symposium on Logic Programming","first-page":"942","article-title":"Uses of higher-order unification for implementing programs transformers","author":"Hannan","year":"1988"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50018-7_bb0310","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50018-7_bb0315","doi-asserted-by":"crossref","first-page":"201","DOI":"10.2307\/2267403","article-title":"Banishing the rule of substitution for functional variables","volume":"18","author":"Henkin","year":"1953","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0320","series-title":"Introduction to combinators and \u03bb-calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0325","series-title":"To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism","article-title":"The formul\u00e6-as-type notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0330","article-title":"Constrained resolution: a complete method for higher order logic","author":"Huet","year":"1972","journal-title":"PhD thesis, Case Western University"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0335","series-title":"International Joint Conference on Artificial Intelligence","first-page":"139","article-title":"A mechanization of type theory","author":"Huet","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0340","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","article-title":"The undecidability of unification in third order logic","volume":"22","author":"Huet","year":"1973","journal-title":"Information and Control"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0345","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0350","article-title":"R\u00e9solution d'\u00e9quations dans les langages d'ordre 1,2, \u2026, \u03c9","author":"Huet","year":"1976","journal-title":"Th\u00e8se d'\u00e9tat, Universit\u00e9 de Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0355","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","article-title":"Proving and applying program transformations expressed with second order patterns","volume":"11","author":"Huet","year":"1978","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0360","series-title":"Lisp and Functional Programming","first-page":"1","article-title":"Super-combinators, a new implementation method for applicative languages","author":"Hughes","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0365","series-title":"Conference on Automated Deduction","first-page":"620","article-title":"Unification in an extensional lambda calculus with ordered function sorts and constant overloading","author":"Johann","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0370","series-title":"Functional Programming Languages and Computer Architecture","first-page":"190","article-title":"Lambda lifting: transforming programs to recursive equations","author":"Johnsson","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0375","series-title":"Algebraic and Logic Programming, International Joint Conference ALP'97-HOA'97","first-page":"61","article-title":"Higher-order equational unification via explicit substitutions","author":"Kirchner","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0380","series-title":"Ellis Horwood series in computer and their applications","article-title":"Lambda calculus, types and models","author":"Krivine","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0385","series-title":"Rewriting Techniques and Applications","first-page":"332","article-title":"Linear second order unification","author":"Levy","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0390","series-title":"On unification problems in restricted second-order languages","author":"Levy","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0395","series-title":"Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications (RTA'00)","first-page":"156","article-title":"Linear second-order unification and context unification with tree-regular constraints","author":"Levy","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0400","series-title":"The undecidability of \u03bb-definability","author":"Loader","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0405","article-title":"The undecidability of the unification problem for third order languages","author":"Lucchesi","year":"1972","journal-title":"Technical Report CSRR 2060, Department of applied analysis and computer science, University of Waterloo"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0415","article-title":"The implementation of ALF, a proof editor based on Martin-L\u00f6f monomorphic type theory with explicit substitution","author":"Magnusson","year":"1994","journal-title":"Doctoral thesis, Chalmers University and University of G\u00f6teborg"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0415","series-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0420","first-page":"354","article-title":"Enumerable sets are diophantine","volume":"11","author":"Matiyacevich","year":"1970","journal-title":"Soviet Math. Doklady"},{"issue":"192","key":"10.1016\/B978-044450813-3\/50018-7_bb0425","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","article-title":"Higher-order rewrite systems and their confluence","author":"Mayr","year":"1998","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50018-7_bb0430","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"1","author":"Miller","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0435","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","article-title":"Unification under a mixed prefix","volume":"14","author":"Miller","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0440","series-title":"Annual Meeting of the Association for Computational Linguistics","first-page":"247","article-title":"Some uses of higher-order logic in computational linguistics","author":"Miller","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0445","series-title":"Conference on Automated Deduction","first-page":"650","article-title":"Theory and practice of minimal modular higher-order E-unification","author":"M\u00fcller","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0450","article-title":"Un calcul de substitutions explicites pour la repr\u00e9sentation de preuves partielles en th\u00e9orie des types","author":"Mu\u00f1oz","year":"1997","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0455","series-title":"First International Workshop on Explicit Substitutions","article-title":"An explicit substitution notation in a \u03bbprolog implementation","author":"Nadathur","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0460","first-page":"499","article-title":"Higher-order logic programming","volume":"Vol. 5","author":"Nadathur","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0465","series-title":"Conference on Automated Deduction","article-title":"System description: A compiler and abstract machine based implementation of \u03bbprolog","author":"Nadathur","year":"1999"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50018-7_bb0470","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","article-title":"A notation for lambda terms : A generalization of environments","volume":"198","author":"Nadathur","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0475","series-title":"Proceedings of the 14th Int. Conference on Automated Deduction (CADE-14)","first-page":"34","article-title":"On equality up-to constraints over finite trees, context unification, and one-step rewriting","author":"Niehren","year":"1997"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50018-7_bb0480","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0020-0190(00)00036-3","article-title":"On rewrite constraints and context unification","volume":"74","author":"Niehren","year":"2000","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0485","series-title":"Logic in Computer Science","first-page":"342","article-title":"Higher-order critical pairs","author":"Nipkow","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0490","series-title":"Automated Deduction - A Basis for Applications","first-page":"399","article-title":"Higher-order rewriting and equational reasonning","author":"Nipkow","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0495","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00885767","article-title":"Reduction and unification in lambda calculi with a general notion of subtype","volume":"12","author":"Nipkow","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0500","series-title":"Fourth-order matching is decidable","author":"Padovani","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0505","series-title":"Typed Lambda Calculi and Applications","first-page":"335","article-title":"On equivalence classes of interpolation equations","author":"Padovani","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0510","series-title":"Types for Proof and Programs 1995","first-page":"201","article-title":"Decidability of all minimal models","author":"Padovani","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0515","article-title":"Filtrage d'ordre sup\u00e9rieur","author":"Padovani","year":"1996","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0520","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","article-title":"Some results on the length of proofs","volume":"177","author":"Parikh","year":"1973","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0525","series-title":"Typed Lambda Calculi and Applications","first-page":"328","article-title":"Inductive definitions in the system Coq, rules and properties","author":"Paulin-Mohring","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0535","series-title":"Logic and computer science","first-page":"361","article-title":"Isabelle: The next 700 theorem provers","author":"Paulson","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0535","series-title":"Conference on Lisp and Functional Programming","first-page":"153","article-title":"Partial polymorphic type inference and higher-order unification","author":"Pfenning","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0540","series-title":"Logical frameworks","first-page":"149","article-title":"Logic programming in the LF logical framework","author":"Pfenning","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0545","series-title":"Logic in Computer Science","first-page":"74","article-title":"Unification and anti-unification in the calculus of constructions","author":"Pfenning","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0550","first-page":"1063","article-title":"Logical frameworks","volume":"Vol. II","author":"Pfenning","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0555","series-title":"Logic in Computer Science","article-title":"Linear higher-order pre-unification","author":"Pfenning","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0560","first-page":"73","article-title":"Building-in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0565","doi-asserted-by":"crossref","first-page":"452","DOI":"10.2307\/2270331","article-title":"Hauptsatz for higher order logic","volume":"33","author":"Prawitz","year":"1968","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0570","series-title":"Conference on Automated Deduction","first-page":"635","article-title":"Decidable higher-order unification problems","author":"Prehofer","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0575","series-title":"Logic in Computer Science","first-page":"507","article-title":"Higher-order narrowing","author":"Prehofer","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0580","article-title":"Solving higher-order equations: from logic to programming","author":"Prehofer","year":"1995","journal-title":"Doctoral thesis, Technische Universit\u00e4t M\u00fcnchen"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0585","article-title":"Proof, search and computation in general logic","author":"Pym","year":"1990","journal-title":"Doctoral thesis, University of Edinburgh"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0590","series-title":"Principle of Programming Languages","first-page":"254","article-title":"Higher-order equational logic programming","author":"Qian","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0595","series-title":"Joint International Conference and Symposium on Logic Programming","article-title":"Higher-order equational E-unification for arbitrary theories","author":"Qian","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0600","series-title":"International Conference on Constaints in Computational Logic","first-page":"105","article-title":"Modular AC unification of higher-order patterns","author":"Qian","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0605","series-title":"Set theory and its logic","author":"Quine","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0610","series-title":"International Federation for Information Processing Congress","first-page":"63","article-title":"New directions in mechanical theorem proving","author":"Robinson","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0615","first-page":"123","article-title":"A note on mechanizing higher order logic","volume":"5","author":"Robinson","year":"1970","journal-title":"Machine Intelligence"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0620","series-title":"R\u00e9solution d'\u00e9quations dans le syst\u00e8me T de G\u00f6del","author":"Sa\u00efdi","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0625","article-title":"Unification of stratified second-order terms","author":"Schmidt-Schauss","year":"1994","journal-title":"Technical Report 12, J.W. Goethe-Universit\u00e4t, Frankfurt"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0630","article-title":"Decidability of bounded second order unification","author":"Schmidt-Schauss","year":"1999","journal-title":"Technical Report 11, J.W. Goethe-Universit\u00e4t, Frankfurt"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0635","series-title":"Conference on Automated Deduction","first-page":"67","article-title":"Solvability of context equations with two context variables is decidable","author":"Schmidt-Schauss","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0640","series-title":"Theory and Practice of Software Development","first-page":"441","article-title":"Linear interpolation for the higher order matching problem","author":"Schubert","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0645","series-title":"Principle of Programming Languages","first-page":"279","article-title":"Second-order unification and type inference for Church-style polymorphism","author":"Schubert","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0650","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF02276799","article-title":"Definierbare Funktionen im \u03bb-Kalk\u00fcl mit Typen","volume":"17","author":"Schwichtenberg","year":"1976","journal-title":"Archiv Logik Grundlagenforschung"},{"key":"10.1016\/B978-044450813-3\/50018-7_rf0660","series-title":"Conference on Automated Deduction","first-page":"573","article-title":"Higher-order E-unification","author":"Snyder","year":"1990"},{"issue":"1 & 2","key":"10.1016\/B978-044450813-3\/50018-7_bb0660","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","article-title":"Higher order unification revisited: Complete sets of tranformations","volume":"8","author":"Snyder","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0665","article-title":"Algorithms for type theory","author":"Springintveld","year":"1995","journal-title":"Doctoral thesis, Utrecht University"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0670","series-title":"Typed Lambda Calculi and Applications","first-page":"428","article-title":"Third-order matching in presence of type constructors","author":"Springintveld","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0675","series-title":"Higher-order Algebra, Logic and Term Rewriting","first-page":"221","article-title":"Third-order matching in the polymorphic lambda calculus","author":"Springintveld","year":"1995"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50018-7_bb0680","doi-asserted-by":"crossref","first-page":"17","DOI":"10.2307\/2273377","article-title":"Completeness, invariance and \u03bb-definability","volume":"47","author":"Statman","year":"1982","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0685","article-title":"On Statman's completeness theorem","author":"Statman","year":"1992","journal-title":"Technical Report CMU-CS-92-152, Carnegie Mellon University,"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0690","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","article-title":"A proof of cut-elimination in simple type theory","volume":"19","author":"Takahashi","year":"1967","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0695","article-title":"Une th\u00e9orie des constructions inductives","author":"Werner","year":"1994","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0700","series-title":"Principia mathematica","author":"Whitehead","year":"1925"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0705","article-title":"The clausal theory of types","author":"Wolfram","year":"1989","journal-title":"Doctoral thesis, University of Cambridge"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0710","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1987-10304","article-title":"The regular expression description of unifier set in the typed \u03bb-calculus","volume":"X","author":"Zaionc","year":"1987","journal-title":"Fundementa Informaticae"},{"key":"10.1016\/B978-044450813-3\/50018-7_bb0715","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00244393","article-title":"Mechanical procedure for proof construction via closed terms in typed \u03bb-calculus","volume":"4","author":"Zaionc","year":"1988","journal-title":"Journal of Automated Reasoning"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500187?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500187?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,8,14]],"date-time":"2021-08-14T23:35:19Z","timestamp":1628984119000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500187"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":143,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50018-7","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}