{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:00Z","timestamp":1742617200093,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_64","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:20Z","timestamp":1330292420000},"page":"347-361","source":"Crossref","is-referenced-by-count":3,"title":["Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type"],"prefix":"10.1007","author":[{"given":"Roland","family":"Fettig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"L\u00f6chner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"27_CR1","first-page":"1","volume":"664","author":"Y. Akama","year":"1993","unstructured":"Y. Akama. On Mints' reductions for ccc-Calculus. In Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 1\u201312, 1993.","journal-title":"LNCS"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo. Isomorphisms of Types. Birkh\u00e4user, 1995.","DOI":"10.1007\/978-1-4612-2572-0_6"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. A confluent reduction for the extensional typed \u03bbs-calculus with pairs, sums, recursion, and terminal object. In A. Lingas et al., editors, ICALP, volume 697 of LNCS, pages 645\u2013656, 1993.","DOI":"10.1007\/3-540-56939-1_109"},{"key":"27_CR4","unstructured":"D. Duggan. Unification with Extended Patterns. Technical Report CS-93-37, University of Waterloo, 1993. To appear in Theoretical Computer Science."},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"27_CR6","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G. P. Huet. A Unification Algorithm for Typed \u03bb-Calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"27_CR7","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"C. B. Jay and N. Ghani. The virtues of eta-expansion. J. Functional Programming, 5(2):135\u2013154, April 1995.","journal-title":"J. Functional Programming"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"T. Johnsson. Fold-unfold transformations on state monadic interpreters. In K. Hammond et al., editors, Functional programming, Glasgow, Workshops in Computing. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3573-9_9"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"D. Kesner. Reasoning about Layered, Wildcard and Product Patterns. In G. Levi and M. Rodnguez-Artalejo, editors, Algebraic and Logic Programming, volume 850 of LNCS, pages 253\u2013268, 1994.","DOI":"10.1007\/3-540-58431-5_18"},{"key":"27_CR10","unstructured":"J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, 1986."},{"issue":"4","key":"27_CR11","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. Logic Comp., 1(4):497\u2013536, 1991.","journal-title":"J. Logic Comp."},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proc. sixth annual IEEE Symposium on Logic in Computer Science, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Functional unification of higher-order patterns. In Proc. eighth annual IEEE Symposium on Logic in Computer Science, pages 64\u201374, 1993.","DOI":"10.1109\/LICS.1993.287599"},{"issue":"3","key":"27_CR14","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1305\/ndjfl\/1093883461","volume":"22","author":"G. Pottinger","year":"1981","unstructured":"G. Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. Notre Dame J. of Formal Logic, 22(3):264\u2013268, 1981.","journal-title":"Notre Dame J. of Formal Logic"},{"key":"27_CR15","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"W. Snyder and J. Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_64.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:19:01Z","timestamp":1742599141000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_64"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_64","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}