{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:28Z","timestamp":1725663508499},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_157","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:22:37Z","timestamp":1330233757000},"page":"79-93","source":"Crossref","is-referenced-by-count":3,"title":["A combinatory logic approach to higher-order E-unification (extended abstract)"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"F. Barbanera. Adding algebraic rewriting to the Calculus of Constructions: strong normalization preserved. Extended Abstracts, The Second International Workshop on Conditional and Typed Rewriting Systems, Center for Pattern Recognition and Machine Intelligence, 1990.","DOI":"10.1007\/3-540-54317-1_96"},{"key":"7_CR2","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. To appear in Theoretical Computer Science."},{"key":"7_CR3","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. To appear in Information and Computation."},{"key":"7_CR4","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J. A. Bergstra","year":"1986","unstructured":"J. A. Bergstra and J. W. Klop. Conditional rewrite rules: confluence and termination. Journal of Computer and System Sciences 32, pp. 322\u2013362, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"A. Boudet. Unification in a combination of equational theories: an efficient algorithm. In Proceedings of the Tenth Conference on Automated Deduction, Springer-Verlag LNAI 449, pp. 292\u2013307, 1990.","DOI":"10.1007\/3-540-52885-7_95"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, IEEE Press, pp. 82\u201390, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"7_CR7","unstructured":"H. B. Curry, R. Feys. Combinatory Logic, Vol. I, North-Holland, 1958."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"D. J. Dougherty. Adding algebra to the untyped lambda calculus. In Proceedings, Fourth International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 488, pp. 37\u201348, 1991. To appear, Information and Computation.","DOI":"10.1007\/3-540-53904-2_84"},{"key":"7_CR9","unstructured":"D. J. Dougherty. Higher-order unification via combinators. Preprint, 1990. To appear, Theoretical Computer Science."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C. Elliott. Higher-order unification with dependent function types. In Proceedings of the Third International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 355, pp. 121\u2013136, 1989.","DOI":"10.1007\/3-540-51081-8_104"},{"key":"7_CR11","unstructured":"M. Fay. First order unification in an equational theory. Proceedings of the Fourth Workshop on Automated Deduction, 1979."},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. H. Gallier","year":"1989","unstructured":"J. H. Gallier and W. Snyder. Complete sets of transformations for general E- unification. Theoretical Computer Science 67, pp. 203\u2013260, 1989.","journal-title":"Theoretical Computer Science"},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"J. H. Gallier","year":"1989","unstructured":"J. H. Gallier and W. Snyder. Higher-order unification revisited: complete sets of transformations. Journal of Symbolic Computation 8, pp. 101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR14","first-page":"224","volume":"32","author":"R. Hindley","year":"1967","unstructured":"R. Hindley. Axioms for strong reduction in combinatory logic. Journal of Symbolic Computation 32, pp. 224\u2013236, 1967.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR15","unstructured":"J. R. Hindley and J. P. Seldin. Introduction to Combinators and \u03bb-Calculus, Cambridge University Press, 1986."},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science 1, pp. 27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"7_CR17","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based study of unification. In Computational Logic: Essays in Honour of Alan Robinson, ed. J. Lassez and G. Plotkin, MIT Press. To appear."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and M. Okada. A computation Model for executable higher-order algebraic specification languages. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Press, pp. 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"7_CR19","unstructured":"P. Johann. Complete Sets of Transformations for Unification Problems. Dissertation, Wesleyan University, 1991."},{"key":"7_CR20","doi-asserted-by":"crossref","first-page":"213","DOI":"10.2307\/2271659","volume":"2","author":"B. Lercher","year":"1967","unstructured":"B. Lercher. Strong reduction and normal form in combinatory logic. Journal of Symbolic Logic 2, pp. 213\u2013223, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"J. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, Volume B, ed. J. van Leeuwen, MIT Press\/Elsevier, pp. 365\u2013458, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"7_CR22","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems 4, pp. 258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order unification, polymorphism, and subsorts. Extended Abstracts, The Second International Workshop on Conditional and Typed Rewriting Systems, Center for Pattern Recognition and Machine Intelligence, 1990.","DOI":"10.1007\/3-540-54317-1_112"},{"key":"7_CR24","first-page":"200","volume":"488","author":"T. Nipkow","year":"1991","unstructured":"T. Nipkow and Z. Qian. Modular Higher-order E-unification. In Proceedings, Fourth International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 488, pp. 200\u2013214, 1991.","journal-title":"Springer-Verlag LNCS"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"M. Okada. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent rewrite system. In Proceedings, ISSAC 89, 1989.","DOI":"10.1145\/74540.74582"},{"key":"7_CR26","unstructured":"S. L. Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987."},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"P. R\u00e9ty. Improving basic narrowing techniques. In Proceedings of the Second International Conference on Rewriting Techniques and Applications, 1987.","DOI":"10.1007\/3-540-17220-3_20"},{"key":"7_CR28","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schauss","year":"1989","unstructured":"M. Schmidt-Schauss. Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation 8, pp. 51\u201399, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR29","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. Siekmann","year":"1989","unstructured":"J. Siekmann. Unification theory. Journal of Symbolic Computation 7, pp. 207\u2013274, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"W. Snyder. Higher-order E-unification. In Proceedings of the Tenth Conference on Automated Deduction, 1990.","DOI":"10.1007\/3-540-52885-7_115"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_157.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:00:04Z","timestamp":1605628804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_157"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_157","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}