{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:58:02Z","timestamp":1770278282095,"version":"3.49.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,5,24]],"date-time":"2011-05-24T00:00:00Z","timestamp":1306195200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10817-011-9229-y","type":"journal-article","created":{"date-parts":[[2011,5,23]],"date-time":"2011-05-23T09:55:45Z","timestamp":1306144545000},"page":"185-207","source":"Crossref","is-referenced-by-count":20,"title":["A Canonical Locally Named Representation of Binding"],"prefix":"10.1007","volume":"49","author":[{"given":"Randy","family":"Pollack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahiko","family":"Sato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,24]]},"reference":[{"key":"9229_CR1","doi-asserted-by":"crossref","unstructured":"Ambler, S.J., Crole, R.L., Momigliano, A.: A definitional approach to primitive recursion over higher order abstract syntax. In: MERLIN \u201903: Proceedings of the 2003 Workshop on Mechanized Reasoning About Languages with Variable Binding, pp. 1\u201311. ACM Press (2003)","DOI":"10.1145\/976571.976572"},{"key":"9229_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles on Programming Languages, pp. 3\u201315. ACM Press (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"9229_CR3","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Parrow, J.: Psi-calculi in isabelle. In: TPHOLs. LNCS, vol. 5674 (2009)","DOI":"10.1007\/978-3-642-03359-9_9"},{"key":"9229_CR4","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Urban, C.: Nominal inversion principles. In: Theorem Proving in Higher Order Logics, TPHOLs 2008. LNCS. Springer-Verlag (2008)","DOI":"10.1007\/978-3-540-71067-7_10"},{"key":"9229_CR5","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol.\u00a01. North Holland (1958)"},{"issue":"5","key":"9229_CR6","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"NG Bruijn de","year":"1972","unstructured":"de\u00a0Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"9229_CR7","unstructured":"Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879) (Translated in van Heijenoort, J.: From Frege to G\u00f6del: a source book in mathematical logic, 1879\u20131931, pp. 1-82. Harvard University Press, Cambridge, MA (1967))"},{"key":"9229_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: Longo, G. (ed.) Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS\u201999), pp. 214\u2013224 (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"9229_CR9","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schliessen. Math. Zeitschrift 39, 176\u2013210 (1934) (English translation in Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North Holland (1969))","journal-title":"Math. Zeitschrift"},{"key":"9229_CR10","unstructured":"Gordon, A.: A mechanism of name-carrying syntax up to alpha-conversion. In: Higher Order Logic Theorem Proving and its Applications. Proceedings, 1993. LNCS 780, pp. 414\u2013426. Springer-Verlag (1993)"},{"key":"9229_CR11","doi-asserted-by":"crossref","unstructured":"Gordon, A., Melham, T.: Five axioms of alpha conversion. In: Von Wright, J., Grundy, J., Harrison, J. (eds.) Ninth Conference on Theorem Proving in Higher Order Logics TPHOL\u201996, Turku. LNCS, vol. 1125, pp. 173\u2013190. Springer-Verlag (1996)","DOI":"10.1007\/BFb0105404"},{"issue":"1","key":"9229_CR12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993) (Preliminary version in LICS\u201987)","journal-title":"J. ACM"},{"key":"9229_CR13","doi-asserted-by":"crossref","unstructured":"Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4\u20135) (2007)","DOI":"10.1017\/S0956796807006430"},{"key":"9229_CR14","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1016\/S1571-0661(04)00323-8","volume":"62","author":"F Honsell","year":"2002","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: The theory of contexts for first order and higher order abstract syntax. Electronic Notes Theor. Comp. Sci. 62, 116\u2013135 (2002)","journal-title":"Electronic Notes Theor. Comp. Sci."},{"key":"9229_CR15","doi-asserted-by":"crossref","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: Bezem, M., Groote, J.F. (eds.) Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA\u201993, Utrecht. LNCS, number 664, pp. 289\u2013305. Springer-Verlag (1993)","DOI":"10.1007\/BFb0037113"},{"issue":"3\u20134","key":"9229_CR16","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1023\/A:1006294005493","volume":"23","author":"J McKinna","year":"1999","unstructured":"McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reason. 23(3\u20134), 373\u2013409 (1999)","journal-title":"J. Autom. Reason."},{"key":"9229_CR17","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: twelf: a meta-logical framework for deductive systems. In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16). LNAI, Springer-Verlag (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"9229_CR18","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"key":"9229_CR19","unstructured":"Pollack, R.: The theory of LEGO: a proof checker for the extended calculus of constructions. Ph.D. thesis, Univ. of Edinburgh (1994)"},{"key":"9229_CR20","doi-asserted-by":"crossref","unstructured":"Pottinger, G.: A tour of the multivariate lambda calculus. In: Dunn, J.M., Gupta, A. (eds.) Truth or Consequences: Essays in Honor of Nuel Belnap. Kluwer (1990)","DOI":"10.1007\/978-94-009-0681-5_14"},{"key":"9229_CR21","volume-title":"Natural Deduction: Proof Theoretical Study","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"9229_CR22","unstructured":"Sato, M.: External and internal syntax of the \u03bb-calculus. In: Buchberger, B., Ida, T., Kutsia, T. (eds.) Proc. of the Austrian-Japanese Workshop on Symbolic Computation in Software Science, SCSS 2008. RISC-Linz Report Series, number 08\u201308, pp. 176\u2013195 (2008)"},{"key":"9229_CR23","doi-asserted-by":"crossref","first-page":"598","DOI":"10.1016\/j.jsc.2010.01.010","volume":"45","author":"M Sato","year":"2010","unstructured":"Sato, M., Pollack, R.: External and internal syntax of the \u03bb-calculus. J. Symb. Comput. 45, 598\u2013616 (2010)","journal-title":"J. Symb. Comput."},{"key":"9229_CR24","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"17","author":"A Stoughton","year":"1988","unstructured":"Stoughton, A.: Substitution revisited. Theor. Comp. Sci. 17, 317\u2013325 (1988)","journal-title":"Theor. Comp. Sci."},{"key":"9229_CR25","doi-asserted-by":"crossref","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s variable convention in rule inductions. In: Automated Deduction\u2014CADE-21. LNCS, number 4603, pp. 35\u201350. Springer-Verlag (2007)","DOI":"10.1007\/978-3-540-73595-3_4"},{"issue":"4","key":"9229_CR26","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in isabelle\/hol. J. Autom. Reason. 40(4), 327\u2013356 (2008)","journal-title":"J. Autom. Reason."},{"key":"9229_CR27","unstructured":"Urban, C., Pollack, R.: Strong induction principles in the locally nameless representation of binders (preliminary notes). Presented at (ACM) Workshop on Mechanizing Metatheory (2007)"},{"key":"9229_CR28","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"J Heijenoort van","year":"1967","unstructured":"van Heijenoort, J.: From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931. Harvard University Press, Cambridge, MA (1967)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9229-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9229-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9229-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T19:28:18Z","timestamp":1741202898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9229-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,24]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["9229"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9229-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,24]]}}}