{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:15:20Z","timestamp":1770279320870,"version":"3.49.0"},"reference-count":31,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T00:00:00Z","timestamp":1340150400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Nominal Isabelle is a definitional extension of the Isabelle\/HOL theorem\nprover. It provides a proving infrastructure for reasoning about programming\nlanguage calculi involving named bound variables (as opposed to de-Bruijn\nindices). In this paper we present an extension of Nominal Isabelle for dealing\nwith general bindings, that means term constructors where multiple variables\nare bound at once. Such general bindings are ubiquitous in programming language\nresearch and only very poorly supported with single binders, such as\nlambda-abstractions. Our extension includes new definitions of\nalpha-equivalence and establishes automatically the reasoning infrastructure\nfor alpha-equated terms. We also prove strong induction principles that have\nthe usual variable convention already built in.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:14)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":20,"title":["General Bindings and Alpha-Equivalence in Nominal Isabelle"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Christian","family":"Urban","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,20]]},"reference":[{"key":"10.2168\/LMCS-8(2:14)2012_Altenkirch10","doi-asserted-by":"crossref","unstructured":"T. Altenkirch, N. A. Danielsson, A. L\u00f6h, and N. Oury. PiSigma: Dependent Types Without the Sugar. InProc. of the 10th International Symposium on Functional and Logic Programming (FLOPS), volume 6009 ofLNCS, pages 40-55, 2010.","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"10.2168\/LMCS-8(2:14)2012_challenge05","doi-asserted-by":"crossref","unstructured":"B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized Metatheory for the Masses: The PoplMark Challenge. InProc. of the 18th Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 ofLNCS, pages 50-65, 2005.","DOI":"10.1007\/11541868_4"},{"key":"10.2168\/LMCS-8(2:14)2012_BengtsonParow09","doi-asserted-by":"crossref","unstructured":"J. Bengtson and J. Parrow. Psi-Calculi in Isabelle. InProc of the 22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 ofLNCS, pages 99-114, 2009.","DOI":"10.1007\/978-3-642-03359-9_9"},{"key":"10.2168\/LMCS-8(2:14)2012_Berghofer99","doi-asserted-by":"crossref","unstructured":"S. Berghofer and M. Wenzel. Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. InProc. of the 12th Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 1690 ofLNCS, pages 19-36, 1999.","DOI":"10.1007\/3-540-48256-3_3"},{"key":"10.2168\/LMCS-8(2:14)2012_chargueraud09","unstructured":"A. Chargu\u00e9raud. The Locally Nameless Representation. To appear inJournal of Automated Reasoning."},{"key":"10.2168\/LMCS-8(2:14)2012_Cheney05a","doi-asserted-by":"crossref","unstructured":"J. Cheney. Scrap Your Nameplate (Functional Pearl). InProc. of the 10th International Conference on Functional Programming (ICFP), pages 180-191, 2005.","DOI":"10.1145\/1090189.1086389"},{"key":"10.2168\/LMCS-8(2:14)2012_Cheney05","doi-asserted-by":"crossref","unstructured":"J. Cheney. Towards a General Theory of Names: Binding and Scope. InProc. of the 3rd ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN), pages 33-40, 2005.","DOI":"10.1145\/1088454.1088459"},{"key":"10.2168\/LMCS-8(2:14)2012_Homeier05","doi-asserted-by":"crossref","unstructured":"P. Homeier. A Design Structure for Higher Order Quotients. InProc. of the 18th Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 ofLNCS, pages 130-146, 2005.","DOI":"10.1007\/11541868_9"},{"key":"10.2168\/LMCS-8(2:14)2012_HuffmanUrban10","doi-asserted-by":"crossref","unstructured":"B. Huffman and C. Urban. Proof Pearl: A New Foundation for Nominal Isabelle. InProc. of the 1st Conference on Interactive Theorem Proving (ITP), volume 6172 ofLNCS, pages 35-50, 2010.","DOI":"10.1007\/978-3-642-14052-5_5"},{"key":"10.2168\/LMCS-8(2:14)2012_KaliszykUrban11","doi-asserted-by":"crossref","unstructured":"C. Kaliszyk and C. Urban. Quotients Revisited for Isabelle\/HOL. InProc. of the 26th ACM Symposium on Applied Computing (SAC), pages 1639-1644, 2011.","DOI":"10.1145\/1982185.1982529"},{"key":"10.2168\/LMCS-8(2:14)2012_Krauss09","doi-asserted-by":"crossref","unstructured":"A. Krauss.Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, TU Munich, 2009.","DOI":"10.1007\/s10817-009-9157-2"},{"key":"10.2168\/LMCS-8(2:14)2012_LeeCraryHarper07","doi-asserted-by":"crossref","unstructured":"D. K. Lee, K. Crary, and R. Harper. Towards a Mechanized Metatheory of Standard ML. InProc. of the 34th Symposium on Principles of Programming Languages (POPL), pages 173-184, 2007.","DOI":"10.1145\/1190216.1190245"},{"key":"10.2168\/LMCS-8(2:14)2012_Leroy92","unstructured":"X. Leroy.Polymorphic Typing of an Algorithmic Language. PhD thesis, University Paris 7, 1992. INRIA Research Report, No 1778."},{"issue":"3-4","key":"10.2168\/LMCS-8(2:14)2012_McKinnaPollack99","first-page":"373","volume":"23","author":"J. McKinna and R. Pollack","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:14)2012_NaraschewskiNipkow99","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1006277616879","volume":"23","author":"W. Naraschewski and T. Nipkow","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:14)2012_pfenningsystem","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. System Description: Twelf - A Meta-Logical Framework for Deductive Systems. InProc. of the 16th International Conference on Automated Deduction (CADE), volume 1632 ofLNAI, pages 202-206, 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"10.2168\/LMCS-8(2:14)2012_Pitts03","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"183","author":"A. M. Pitts","year":"2003","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(2:14)2012_Pitts04","unstructured":"A. M. Pitts. Notes on the Restriction Monad for Nominal Sets and Cpos. Unpublished notes for an invited talk given at CTCS, 2004."},{"key":"10.2168\/LMCS-8(2:14)2012_Pottier06","doi-asserted-by":"crossref","unstructured":"F. Pottier. An Overview of Caml. InProc. of the 7th ACM Workshop on ML, volume 148 ofENTCS, pages 27-52, 2006.","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"10.2168\/LMCS-8(2:14)2012_SatoPollack10","doi-asserted-by":"crossref","first-page":"598","DOI":"10.1016\/j.jsc.2010.01.010","volume":"45","author":"M. Sato and R. Pollack","year":"2010","journal-title":"Journal of Symbolic Computation"},{"key":"10.2168\/LMCS-8(2:14)2012_SewellBestiary","unstructured":"P. Sewell. A Binding Bestiary. Unpublished notes."},{"issue":"1","key":"10.2168\/LMCS-8(2:14)2012_ott-jfp","first-page":"70","volume":"20","author":"P. Sewell, F. Z. Nardelli, S. Owens, G.","year":"2010","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(2:14)2012_CoreHaskell","doi-asserted-by":"crossref","unstructured":"M. Sulzmann, M. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with Type Equality Coercions. InProc. of the 3rd Workshop on Types in Language Design and Implementation (TLDI), pages 53-66, 2007.","DOI":"10.1145\/1190315.1190324"},{"key":"10.2168\/LMCS-8(2:14)2012_TobinHochstadtFelleisen08","doi-asserted-by":"crossref","unstructured":"S. Tobin-Hochstadt and M. Felleisen. The Design and Implementation of Typed Scheme. InProc. of the 35rd Symposium on Principles of Programming Languages (POPL), pages 395-406, 2008.","DOI":"10.1145\/1328438.1328486"},{"key":"10.2168\/LMCS-8(2:14)2012_Traytel12","doi-asserted-by":"crossref","unstructured":"D. Traytel, A. Popescu, and J. C. Blanchette. Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. To appear inProc. of the 27th Symposium on Logic in Computer Science (LICS), 2012.","DOI":"10.1109\/LICS.2012.75"},{"issue":"4","key":"10.2168\/LMCS-8(2:14)2012_Urban08","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:14)2012_UrbanCheneyBerghofer08","doi-asserted-by":"crossref","unstructured":"C. Urban, J. Cheney, and S. Berghofer. Mechanizing the Metatheory of LF. InProc. of the 23rd Symposium on Logic in Computer Science (LICS), pages 45-56, 2008.","DOI":"10.1109\/LICS.2008.29"},{"key":"10.2168\/LMCS-8(2:14)2012_UrbanKaliszyk11","doi-asserted-by":"crossref","unstructured":"C. Urban and C. Kaliszyk. General Bindings and Alpha-Equivalence in Nominal Isabelle. InProc. of the 20th European Symposium on Programming (ESOP), volume 6602 ofLNCS, pages 480-500, 2011.","DOI":"10.1007\/978-3-642-19718-5_25"},{"key":"10.2168\/LMCS-8(2:14)2012_UrbanNipkow09","doi-asserted-by":"crossref","unstructured":"C. Urban and T. Nipkow. Nominal Verification of Algorithm W. In G. Huet, J.-J. L\u00e9vy, and G. Plotkin, editors,From Semantics to Computer Science. Essays in Honour of Gilles Kahn, pages 363-382. Cambridge University Press, 2009.","DOI":"10.1017\/CBO9780511770524.017"},{"key":"10.2168\/LMCS-8(2:14)2012_UrbanZhu08","doi-asserted-by":"crossref","unstructured":"C. Urban and B. Zhu. Revisiting Cut-Elimination: One Difficult Proof is Really a Proof. InProc. of the 9th International Conference on Rewriting Techniques and Applications (RTA), volume 5117 ofLNCS, pages 409-424, 2008.","DOI":"10.1007\/978-3-540-70590-1_28"},{"key":"10.2168\/LMCS-8(2:14)2012_WeirichYorgeySheard11","doi-asserted-by":"crossref","unstructured":"S. Weirich, B. Yorgey, and T. Sheard. Binders Unbound. InProc. of the 16th International Conference on Functional Programming (ICFP), pages 333-345, 2011.","DOI":"10.1145\/2034773.2034818"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/813\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/813\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:35Z","timestamp":1681242995000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/813"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,20]]},"references-count":31,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:14)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.0136","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.0136","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1017\/s0956796819000170","asserted-by":"subject"},{"id-type":"handle","id":"2066\/213879","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,20]]},"article-number":"813"}}