{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T08:46:25Z","timestamp":1651135585544},"reference-count":29,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5403,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1998,10]]},"DOI":"10.1016\/s0304-3975(97)00141-2","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T19:40:02Z","timestamp":1049744402000},"page":"1-50","source":"Crossref","is-referenced-by-count":3,"title":["Unification with extended patterns"],"prefix":"10.1016","volume":"206","author":[{"given":"Dominic","family":"Duggan","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S0304-3975(97)00141-2_BIB1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","article-title":"Explicit substitutions","volume":"1","author":"Abadi","year":"1991","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB2","doi-asserted-by":"crossref","unstructured":"D. Duggan, Higher-order substitutions, Information and Computation, to appear.","DOI":"10.1006\/inco.2000.2887"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB3","unstructured":"D. Duggan, Metaprogramming with higher-order abstract syntax, products and polymorphism, submitted for publication."},{"key":"10.1016\/S0304-3975(97)00141-2_BIB4","article-title":"Some extensions and applications of higher order unification","author":"Elliott","year":"1988"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB5","article-title":"Higer-order unification with dependent types, Rewriting Techniques and Applications","volume":"vol. 355","author":"Elliott","year":"1989"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB6","article-title":"Extensions and Applications of Higher-Order Unification","author":"Elliott","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB7","series-title":"Proc. ACM Symp. on Principles of Programming Languages","first-page":"1","article-title":"On laziness and optimality in lambda interpreters: tools for specification and analysis","author":"Field","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB8_1","article-title":"On Girard's \u2018candidats de reducibilit\u00e9\u2019","author":"Gallier","year":"1990","journal-title":"Technical report, University of Pennsylvania, Philadelphia, PA"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB8_2","series-title":"Logic, and Comput. Science","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB9","series-title":"Proc. IEEE Symp. on Logic in Computer Science","first-page":"453","article-title":"The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi","author":"Geuvers","year":"1992"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB10","article-title":"Interpr\u00e9tation Fonctionelle et Elimination des Coupures dans l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur","author":"Girard","year":"1972","journal-title":"Ph.D. Thesis, Th\u00e8se de Doctorat d'\u00c9tat"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB11","series-title":"Proc. ACM Symp. on Principles of Programming Languages, Association for Computing Machinery","first-page":"341","article-title":"Higher-order modules and the phase distinction","author":"Harper","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB12","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":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00141-2_BIB13","series-title":"Proc. IEEE Symp. on Logic in Computer Science, IEEE Press","first-page":"385","article-title":"ECC, an extended calculus of constructions","author":"Luo","year":"1989"},{"issue":"4","key":"10.1016\/S0304-3975(97)00141-2_BIB14","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":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(97)00141-2_BIB15","series-title":"Proc. Internat. Conf. on Logic Programming, MIT Press","first-page":"255","article-title":"Unification of simply typed \u03bb-terms as logic programming","author":"Miller","year":"1991"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB16","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":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(97)00141-2_BIB17","series-title":"Proc. Internat. Conf. on Logic Programming, MIT Press","first-page":"810","article-title":"An overview of \u03bb-Prolog","author":"Nadathur","year":"1988"},{"issue":"4","key":"10.1016\/S0304-3975(97)00141-2_BIB18","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1145\/96559.96570","article-title":"Higher-order Horn clauses","volume":"37","author":"Nadathur","year":"1990","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(97)00141-2_BIB19","series-title":"Proc. ACM Symp. on Lisp and Functional Progamming, Association for Computing Machinery","first-page":"341","article-title":"A representation of lambda terms suitable for operations on their intensions","author":"Nadathur","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB20","series-title":"Proc. IEEE Symp. on Logic in Computer Science, IEEE Press","first-page":"342","article-title":"Higher order critical pairs","author":"Nipkow","year":"1991"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB21","series-title":"Proc. IEEE Symp. on Logic in Computer Science, IEEE Press","article-title":"Functional unification of higher-order patterns","author":"Nipkow","year":"1993"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB22","series-title":"Logic and Computer Science","first-page":"361","article-title":"Isabelle: the next 700 theorem provers","author":"Paulson","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB23","series-title":"Proc. IEEE Symp. on Logic in Computer Science, IEEE Press","first-page":"313","article-title":"Elf: a language for logic definition and verified metaprogramming","author":"Pfenning","year":"1989"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB24","series-title":"Logical Frameworks","first-page":"149","article-title":"Logic programming in the LF logical framework","author":"Pfenning","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB25","series-title":"Proc. IEEE Symp. on Logic in Computer Science","article-title":"Unification and anti-unification in the calculus of constructions","author":"Pfenning","year":"1991"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB26","series-title":"Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, Association for Computing Machinery","first-page":"199","article-title":"Higher-order abstract syntax","author":"Pfenning","year":"1988"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB27","article-title":"Proofs, search and computation in general logic","author":"Pym","year":"1990"},{"key":"10.1016\/S0304-3975(97)00141-2_BIB28","series-title":"Proc. Coll. on Trees in Algebra and Programming","first-page":"391","article-title":"Linear unification of higher-order patterns","volume":"vol. 668","author":"Qian","year":"1993"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001412?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001412?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T13:02:14Z","timestamp":1555419734000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397597001412"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,10]]},"references-count":29,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,10]]}},"alternative-id":["S0304397597001412"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(97)00141-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1998,10]]}}}