{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T05:21:48Z","timestamp":1738387308913,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-70590-1_17","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"246-260","source":"Crossref","is-referenced-by-count":15,"title":["Nominal Unification from a Higher-Order Perspective"],"prefix":"10.1007","author":[{"given":"Jordi","family":"Levy","sequence":"first","affiliation":[]},{"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"17_CR1","first-page":"25","volume":"176","author":"C. Calv\u00e8s","year":"2007","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: Implementing nominal unification. ENTCS\u00a0176(1), 25\u201337 (2007)","journal-title":"ENTCS"},{"key":"17_CR2","unstructured":"Cheney, J.: Relating higher-order pattern unification and nominal unification. In: Proc. of the 19th Int.\u00a0Work on Unification, UNIF 2005, pp. 104\u2013119 (2005)"},{"key":"17_CR3","first-page":"223","volume":"1496","author":"R.A. Clouston","year":"2007","unstructured":"Clouston, R.A., Pitts, A.M.: Nominal equational logic. ENTCS\u00a01496, 223\u2013257 (2007)","journal-title":"ENTCS"},{"key":"17_CR4","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.: \u03b1-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":"17_CR5","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Higher-order unification and matching. Handbook of automated reasoning, pp. 1009\u20131062 (2001)","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Fern\u00e1ndez, M., Gabbay, M.: Nominal rewriting with name generation: abstraction vs. locality. In: Proc.\u00a0of the 7th Int.\u00a0Conf.\u00a0on Principles and Practice of Declarative Programming, PPDP 2005, pp. 47\u201358 (2005)","DOI":"10.1145\/1069774.1069779"},{"issue":"6","key":"17_CR7","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","volume":"205","author":"M. Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.: Nominal rewriting. Information and Computation\u00a0205(6), 917\u2013965 (2007)","journal-title":"Information and Computation"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, M., Cheney, J.: A sequent calculus for nominal logic. In: Proc. of the 19th Symp. on Logic in Computer Science, LICS 2004, pp. 139\u2013148 (2004)","DOI":"10.1109\/LICS.2004.1319608"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013, 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Gabbay, M., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Proc.\u00a0of the 14th Symp.\u00a0on Logic in Computer Science, LICS 1999, pp. 214\u2013224 (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BFb0052360","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"1998","unstructured":"Levy, J.: Decidable and undecidable second-order unification problems. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 47\u201360. Springer, Heidelberg (1998)"},{"key":"17_CR12","unstructured":"Lucchesi, C.L.: The undecidability of the unification problem for third-order languages. Technical Report CSRR 2059, Dept. of Applied Analysis and Computer Science, Univ. of Waterloo (1972)"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Levy, J., Veanes, M.: On the undecidability of second-order unification. Information and Computation\u00a0159, 125\u2013150 (2000)","journal-title":"Information and Computation"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"J. of Logic and Computation"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Proc. of the 8th Symp.\u00a0on Logic in Computer Science, LICS 1993, pp. 64\u201374 (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-45500-0_11","volume-title":"Theoretical Aspects of Computer Software","author":"A.M. Pitts","year":"2001","unstructured":"Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 219\u2013242. Springer, Heidelberg (2001)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"issue":"3","key":"17_CR18","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1093\/logcom\/6.3.315","volume":"6","author":"Z. Qian","year":"1996","unstructured":"Qian, Z.: Unification of higher-order patterns in linear time and space. J. of Logic and Computation\u00a06(3), 315\u2013341 (1996)","journal-title":"J. of Logic and Computation"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/11417170_29","volume-title":"Typed Lambda Calculi and Applications","author":"C. Urban","year":"2005","unstructured":"Urban, C., Cheney, J.: Avoiding equivariance in alpha-prolog. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 401\u2013416. Springer, Heidelberg (2005)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/978-3-540-45220-1_41","volume-title":"Computer Science Logic","author":"C. Urban","year":"2003","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 513\u2013527. Springer, Heidelberg (2003)"},{"key":"17_CR21","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.J.: Nominal unification. Theoretical Computer Science\u00a0323, 473\u2013497 (2004)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:14:31Z","timestamp":1738325671000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540705888","9783540705901"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}