{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:32Z","timestamp":1725489332632},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_35","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T12:03:26Z","timestamp":1187265806000},"page":"522-537","source":"Crossref","is-referenced-by-count":5,"title":["Decidability of Bounded Higher-Order Unification"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus U.","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"35_CR1","unstructured":"Peter Andrews. An introduction to mathematical logic and type theory: to truth through proof. Academic Press, 1986"},{"key":"35_CR2","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"Henk P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, New York, 1984"},{"key":"35_CR3","doi-asserted-by":"crossref","unstructured":"Henk P. Barendregt. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science: Formal Models and Semantics, volume B, chapter 7, pages 321\u2013363. Elsevier, 1990","DOI":"10.1016\/B978-0-444-88074-1.50012-3"},{"key":"35_CR4","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.2307\/2695106","volume":"66","author":"A. Beckmann","year":"2001","unstructured":"Arnold Beckmann. Exact bounds for lengths of reductions in typed \u03bc-calculus. J. Symbolic Logic, 66:1277\u20131285, 2001","journal-title":"J. Symbolic Logic"},{"key":"35_CR5","unstructured":"Richard Bird. Introduction to Functional Programming using Haskell. Prentice Hall, 1998"},{"key":"35_CR6","unstructured":"Franz Baader and J\u00f6rg Siekmann. Unification theory. In D.M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41\u2013125. Oxford University Press, 1994"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Rodney.G. Downey and Michael R. Fellows. Parametrized Complexity. Springer, 1999","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science: Formal Models and Semantics, volume B, chapter 6, pages 243\u2013320. Elsevier, 1990","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Gilles Dowek. Higher-order unification and matching. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 16, pages 1009\u20131062. North-Holland, 2001","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"35_CR10","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"W. A. Farmer","year":"1988","unstructured":"W. A. Farmer. A unification algorithm for second order monadic terms. Annals of Pure and Applied Logic, 39:131\u2013174, 1988","journal-title":"Annals of Pure and Applied Logic"},{"key":"35_CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W. A. Farmer","year":"1991","unstructured":"W. A. Farmer. Simple second-order languages for which unification is undecidable. J. Theoretical Computer Science, 87:173\u2013214, 1991","journal-title":"J. Theoretical Computer Science"},{"key":"35_CR12","unstructured":"Robin O. Gandy. Proofs of strong normalization. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457\u2013477. Academic Press, 1980"},{"key":"35_CR13","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"Warren. D. Goldfarb","year":"1981","unstructured":"Warren. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981","journal-title":"Theoretical Computer Science"},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"J. Roger Hindley. Basic simple type theory. Cambridge tracts in theoretical computer science. Cambridge University Press, 1997","DOI":"10.1017\/CBO9780511608865"},{"key":"35_CR15","unstructured":"M. Hanus, H. Kuchen, and J. J. Moreno-Navarro. Curry: A truly functional logic language. In Proc. ILPS\u201995 Workshop on Visions for the Future of Logic Programming, pages 95\u2013107, 1995"},{"key":"35_CR16","unstructured":"J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and \u03bb-calculus. Cambridge University Press, 1986"},{"key":"35_CR17","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G\u00e9rard Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975","journal-title":"Theoretical Computer Science"},{"key":"35_CR18","unstructured":"Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 2\u2013116. Oxford University Press, 1992"},{"key":"35_CR19","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Jordi Levy and Margus Veanes. On the undecidability of second-order unification. Information and Computation, 159:125\u2013150, 2000","journal-title":"Information and Computation"},{"issue":"4","key":"35_CR20","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Dale Miller. A logic programming language with lambda-abstraction, function variables and simple unification. J. of Logic and Computation, 1(4):497\u2013536, 1991","journal-title":"J. of Logic and Computation"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. LICS, pages 342\u2013349, 1991","DOI":"10.1109\/LICS.1991.151658"},{"key":"35_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 17, pages 1063\u20131147. North-Holland, 2001","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Helmut Schwichtenberg. Complexity of normalization in the pure typed \u03bb-calculus. In A. S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference hold in Noordwijkerhout, 8\u201313 June, 1981, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 453\u2013458. North Holland, 1982","DOI":"10.1016\/S0049-237X(09)70143-0"},{"key":"35_CR25","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01621476","volume":"30","author":"H. Schwichtenberg","year":"1991","unstructured":"Helmut Schwichtenberg. An upper bound for reduction sequences in the typed \u03bb-calculus. Archive for Mathematical Logic, 30:405\u2013408, 1991. Dedicated to Kurt Sch\u00fctte on the occasion of his 80th birthday","journal-title":"Archive for Mathematical Logic"},{"key":"35_CR26","unstructured":"Manfred Schmidt-Schau\u00df. Decidability of bounded second order unification. Frank report 11, FB Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main, 1999. available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/articles.html"},{"key":"35_CR27","volume-title":"Frank-Report 12","author":"M. Schmidt-Schau\u00df","year":"1999","unstructured":"Manfred Schmidt-Schau\u00df. A decision algorithm for stratified context unification. Frank-Report 12, Fachbereich Informatik, J. W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany, 1999. accepted for publication in J. Logic and Computation, available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/articles.html"},{"key":"35_CR28","doi-asserted-by":"crossref","unstructured":"Manfred Schmidt-Schau\u00df. Decidability of bounded second order unification, 2001. submitted for publication","DOI":"10.1007\/3-540-45793-3_35"},{"key":"35_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0052361","volume-title":"Proceedings of the 9th Int. Conf. on Rewriting Techniques and Applications","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"Manfred Schmidt-Schau\u00df and Klaus U. Schulz. On the exponent of periodicity of minimal solutions of context equations. In Proceedings of the 9th Int. Conf. on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 61\u201375, 1998"},{"key":"35_CR30","unstructured":"Manfred Schmidt-Schau\u00df and Klaus U. Schulz. Decidability of bounded higher order unification. Frank report 15, Institut f\u00fcr Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main, 2001. also appeared as: Forschungsbericht, Centrum f\u00fcr Informations-und Sprachverarbeitung, Universit\u00e9t M\u00fcnchen. The paper is available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/articles.html"},{"issue":"1","key":"35_CR31","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1006\/jsco.2001.0438","volume":"33","author":"M. Schmidt-Schau\u00df","year":"2002","unstructured":"Manfred Schmidt-Schau\u00df and Klaus U. Schulz. Solvability of context equations with two context variables is decidable. Journal of Symbolic Computation, 33(1):77\u2013122, 2002","journal-title":"Journal of Symbolic Computation"},{"key":"35_CR32","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0020-0190(00)00029-6","volume":"74","author":"M. Veanes","year":"2000","unstructured":"Margus Veanes. Farmer\u2019s theorem revisited. Information Processing Letters, 74:47\u201353, 2000","journal-title":"Information Processing Letters"},{"key":"35_CR33","unstructured":"ToMasz Wierzbicki. A decidable variant of the higher order matching. In Proc. RTA\u2019 02, 2002 to appear."},{"key":"35_CR34","doi-asserted-by":"crossref","unstructured":"David A. Wolfram. The clausal theories of types. Number 21 in Cambridge tracts in theoretical computer science. Cambridge University Press, 1993","DOI":"10.1017\/CBO9780511569906"},{"key":"35_CR35","first-page":"120","volume":"5","author":"A.P. Zhezherun","year":"1979","unstructured":"A.P Zhezherun. Decidability of the unification problem for second order languages with unary function symbols. Kibernetika (Kiev), 5:120\u2013125, 1979. Translated as Cybernetics 15(5): 735\u2013741,1980","journal-title":"Kibernetika (Kiev)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:34:21Z","timestamp":1556771661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}