{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:11:37Z","timestamp":1763388697658},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540226710"},{"type":"electronic","value":"9783540277750"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27775-0_19","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T20:29:36Z","timestamp":1284582576000},"page":"269-283","source":"Crossref","is-referenced-by-count":35,"title":["\u03b1Prolog: A Logic Programming Language with Names, Binding and \u03b1-Equivalence"],"prefix":"10.1007","author":[{"given":"James","family":"Cheney","sequence":"first","affiliation":[]},{"given":"Christian","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding","author":"A. Andreas","year":"2001","unstructured":"Andreas, A.: A third-order representation of the \u03bb\u03bc-calculus. In: MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding. Electronic Notes in Theoretical Computer Science, vol.\u00a058(1), Elsevier, Amsterdam (2001)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-27836-8_30","volume-title":"Automata, Languages and Programming","author":"J. Cheney","year":"2004","unstructured":"Cheney, J.: The complexity of equivariant unification. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 332\u2013344. Springer, Heidelberg (2004)"},{"issue":"5","key":"19_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat.\u00a034(5), 381\u2013392 (1972)","journal-title":"Indag. Mat."},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 124\u2013138. Springer, Heidelberg (1995)"},{"key":"19_CR5","first-page":"193","volume-title":"Proc. 14th Symp. on Logic in Computer Science (LICS 1999)","author":"M.P. Fiore","year":"1999","unstructured":"Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. 14th Symp. on Logic in Computer Science (LICS 1999), pp. 193\u2013202. IEEE, Los Alamitos (1999)"},{"key":"19_CR6","volume-title":"Thirty-five years of Automath","author":"M.J. Gabbay","year":"2003","unstructured":"Gabbay, M.J.: The \u03c0-calculus in FM. In: Kamareddine, F. (ed.) Thirty-five years of Automath, Kluwer, Dordrecht (2003)"},{"key":"19_CR7","unstructured":"Gabbay, M.J., Cheney, J.: A proof theory for nominal logic. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004 (2004) (to appear)"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2002","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing\u00a013, 341\u2013363 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-45500-0_12","volume-title":"Theoretical Aspects of Computer Software","author":"M. Hamana","year":"2001","unstructured":"Hamana, M.: A logic programming language based on binding algebras. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 243\u2013262. Springer, Heidelberg (2001)"},{"key":"19_CR10","first-page":"204","volume-title":"Proc. 14th Symp. on Logic in Computer Science","author":"M. Hofmann","year":"1999","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proc. 14th Symp. on Logic in Computer Science, July 1999, pp. 204\u2013213. IEEE, Los Alamitos (1999)"},{"issue":"1-3","key":"19_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(98)10002-X","volume":"37","author":"J. Jaffar","year":"1998","unstructured":"Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The semantics of constraint logic programs. Journal of Logic Programming\u00a037(1-3), 1\u201346 (1998)","journal-title":"Journal of Logic Programming"},{"issue":"4","key":"19_CR12","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. Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"J. Logic and Computation"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic\u00a051, 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I-II. Information and Computation\u00a0100(1), 1\u201377 (1992)","journal-title":"Information and Computation"},{"key":"19_CR15","first-page":"267","volume-title":"Informatics Research Report EDI-INF-RR-0046, Supplemental Proceedings of TPHOLs 2001","author":"A. Momigliano","year":"2001","unstructured":"Momigliano, A., Ambler, S.J., Crole, R.L.: A comparison of formalizations of the meta-theory of a language with variable bindings in Isabelle. In: Informatics Research Report EDI-INF-RR-0046, Supplemental Proceedings of TPHOLs 2001, pp. 267\u2013282. University of Edinburgh, Edinburgh (2001)"},{"key":"19_CR16","first-page":"499","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"G. Nadathur","year":"1998","unstructured":"Nadathur, G., Miller, D.: Higher-order logic programming. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a05, ch. 8, pp. 499\u2013590. Oxford University Press, Oxford (1998)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"19_CR18","first-page":"199","volume-title":"Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 1989)","author":"F. Pfenning","year":"1989","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 1989), pp. 199\u2013208. ACM Press, New York (1989)"},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"183","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0183, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"19_CR20","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding","author":"C. R\u00f6ckl","year":"2001","unstructured":"R\u00f6ckl, C.: A first-order syntax for the pi-calculus in isabelle\/hol using permutations. In: Ambler, S.J., Crole, R.L., Momigliano, A. (eds.) MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding. Electronic Notes in Theoretical Computer Science, vol.\u00a058(1), Elsevier, Amsterdam (2001)"},{"key":"19_CR21","unstructured":"Sch\u00fcrmann, C., Fontana, R., Liao, Y.: Delphin: Functional programming with deductive systems (2002), Available at \n                      \n                        http:\/\/cs-www.cs.yale.edu\/homes\/carsten\/"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/944705.944729","volume-title":"Proc. 8th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2003)","author":"M.R. Shinwell","year":"2003","unstructured":"Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programmming with binders made simple. In: Proc. 8th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2003), Uppsala, Sweden, pp. 263\u2013274. ACM Press, New York (2003)"},{"issue":"1-3","key":"19_CR23","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0743-1066(96)00068-4","volume":"29","author":"Z. Somogyi","year":"1996","unstructured":"Somogyi, Z., Henderson, F., Conway, T.: The execution algorithm of Mercury: an efficient purely declarative logic programming language. J. Logic Programming\u00a029(1-3), 17\u201364 (1996)","journal-title":"J. Logic Programming"},{"key":"19_CR24","volume-title":"Meta-Programming in Logic Programming","author":"J. Staples","year":"1996","unstructured":"Staples, J., Robinson, P.J., Paterson, R.A., Hagen, R.A., Craddock, A.J., Wallis, P.C.: Qu-prolog: An extended prolog for meta level programming. In: Abramson, H., Rogers, M.H. (eds.) Meta-Programming in Logic Programming, ch.\u00a023, MIT Press, Cambridge (1996)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"19_CR26","unstructured":"Urban, C., Cheney, J.: Avoiding equivariant unification (submitted)"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27775-0_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:24:37Z","timestamp":1620012277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27775-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540226710","9783540277750"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27775-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}