{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:18:09Z","timestamp":1770275889315,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_6","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T10:23:14Z","timestamp":1278930194000},"page":"51-66","source":"Crossref","is-referenced-by-count":12,"title":["(Nominal) Unification by Recursive Descent with Triangular Substitutions"],"prefix":"10.1007","author":[{"given":"Ramana","family":"Kumar","sequence":"first","affiliation":[]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst.\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"6_CR2","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"Paterson, M., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci.\u00a016(2), 158\u2013167 (1978)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2-3","key":"6_CR3","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/j.tcs.2008.05.012","volume":"403","author":"C. Calv\u00e8s","year":"2008","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: A polynomial nominal unification algorithm. Theor. Comput. Sci.\u00a0403(2-3), 285\u2013306 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-70590-1_17","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"2008","unstructured":"Levy, J., Villaret, M.: Nominal unification from a higher-order perspective. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 246\u2013260. Springer, Heidelberg (2008)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K. Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, M.Z. (eds.) KI 2009. LNCS, vol.\u00a05803, pp. 435\u2013443. Springer, Heidelberg (2009)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"6_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5801.001.0001","volume-title":"The Reasoned Schemer","author":"D.P. Friedman","year":"2005","unstructured":"Friedman, D.P., Byrd, W.E., Kiselyov, O.: The Reasoned Schemer. The MIT Press, Cambridge (2005)"},{"key":"6_CR8","unstructured":"Byrd, W.E.: Relational Programming in miniKanren: Techniques, Applications, and Implementations. PhD thesis, Indiana University (2009)"},{"issue":"1-3","key":"6_CR9","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C. Urban","year":"2004","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.: Nominal unification. Theor. Comput. Sci.\u00a0323(1-3), 473\u2013497 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-540-27775-0_19","volume-title":"Logic Programming","author":"J. Cheney","year":"2004","unstructured":"Cheney, J., Urban, C.: alpha-Prolog: A logic programming language with names, binding and \u03b1-equivalence. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol.\u00a03132, pp. 269\u2013283. Springer, Heidelberg (2004)"},{"key":"6_CR11","unstructured":"Byrd, W.E., Friedman, D.P.: alphaKanren: A fresh name in nominal logic programming languages. Scheme and Functional Programming (2007)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0167-6423(85)90009-7","volume":"5","author":"L.C. Paulson","year":"1985","unstructured":"Paulson, L.C.: Verifying the unification algorithm in LCF. Sci. Comput. Program.\u00a05(2), 143\u2013169 (1985)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"6_CR13","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1017\/S0956796803004957","volume":"13","author":"C. McBride","year":"2003","unstructured":"McBride, C.: First-order unification by structural recursion. J. Funct. Program.\u00a013(6), 1061\u20131075 (2003)","journal-title":"J. Funct. Program."},{"issue":"1-2","key":"6_CR14","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10817-006-9030-5","volume":"37","author":"J.L. Ruiz-Reina","year":"2006","unstructured":"Ruiz-Reina, J.L., Mart\u00edn-Mateos, F.J., Alonso, J.A., Hidalgo, M.J.: Formal correctness of a quadratic unification algorithm. J. Autom. Reasoning\u00a037(1-2), 67\u201392 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR15","unstructured":"Urban, C.: Nominal unification (2004), http:\/\/www4.in.tum.de\/~urbanc\/Unification\/"},{"issue":"1","key":"6_CR16","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.entcs.2006.09.027","volume":"176","author":"C. Calv\u00e8s","year":"2007","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: Implementing nominal unification. Electr. Notes Theor. Comput. Sci.\u00a0176(1), 25\u201337 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/1292535.1292541","volume-title":"ML","author":"S. Conchon","year":"2007","unstructured":"Conchon, S., Filli\u00e2tre, J.C.: A persistent union-find data structure. In: Russo, C.V., Dreyer, D. (eds.) ML, pp. 37\u201346. ACM, New York (2007)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:47:04Z","timestamp":1606168024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}