{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:08Z","timestamp":1750810208657,"version":"3.41.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_16","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"241-261","source":"Crossref","is-referenced-by-count":7,"title":["A Formalized General Theory of Syntax with\u00a0Bindings"],"prefix":"10.1007","author":[{"given":"Lorenzo","family":"Gheri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"The POPLmark Challenge (2009). http:\/\/fling-l.seas.upenn.edu\/plclub\/cgi-bin\/poplmark\/"},{"issue":"5","key":"16_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.entcs.2007.01.028","volume":"174","author":"BE Aydemir","year":"2007","unstructured":"Aydemir, B.E., Bohannon, A., Weirich, S.: Nominal reasoning techniques in Coq: (extended abstract). Electron. Notes Theor. Comput. Sci. 174(5), 69\u201377 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008, pp. 3\u201315 (2008)","DOI":"10.1145\/1328897.1328443"},{"key":"16_CR4","volume-title":"The Lambda Calculus","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus. North-Holland, Amsterdam (1984)"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9336-2","volume":"56","author":"J Bengtson","year":"2016","unstructured":"Bengtson, J., Parrow, J., Weber, T.: Psi-calculi in Isabelle. J. Autom. Reason. 56(1), 1\u201347 (2016)","journal-title":"J. Autom. Reason."},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL \u2014 lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19\u201336. Springer, Heidelberg (1999). doi:10.1007\/3-540-48256-3_3"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-40885-4_17","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 245\u2013260. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40885-4_17"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493\u2013507. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-36742-7_34"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-662-54434-1_5","volume-title":"Programming Languages and Systems","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits - implementing corecursion in foundational proof assistants. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 111\u2013140. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54434-1_5"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). doi:10.1007\/978-3-319-08970-6_7"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: LICS. IEEE (2017)","DOI":"10.1109\/LICS.2017.8005071"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-08970-6_8","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 111\u2013127. Springer, Cham (2014). doi:10.1007\/978-3-319-08970-6_8"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-319-08587-6_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness\u2014a coinductive pearl. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 46\u201360. Springer, Cham (2014). doi:10.1007\/978-3-319-08587-6_4"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: ICFP, pp. 192\u2013204 (2015)","DOI":"10.1145\/2858949.2784732"},{"issue":"1","key":"16_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017)","journal-title":"J. Autom. Reason."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Chlipala, A.J.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143\u2013156 (2008)","DOI":"10.1145\/1411203.1411226"},{"key":"16_CR17","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. 902, pp. 124\u2013138. Springer, Heidelberg (1995). doi:10.1007\/BFb0014049"},{"issue":"1","key":"16_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-010-9194-x","volume":"48","author":"AP Felty","year":"2012","unstructured":"Felty, A.P., Momigliano, A.: Hybrid - a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48(1), 43\u2013105 (2012)","journal-title":"J. Autom. Reason."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding (extended abstract). In: LICS 1999, pp. 193\u2013202 (1999)","DOI":"10.1109\/LICS.1999.782615"},{"issue":"7","key":"16_CR20","doi-asserted-by":"publisher","first-page":"982","DOI":"10.1016\/j.ic.2006.10.010","volume":"205","author":"MJ Gabbay","year":"2007","unstructured":"Gabbay, M.J.: A general mathematics of names. Inf. Comput. 205(7), 982\u20131011 (2007)","journal-title":"Inf. Comput."},{"key":"16_CR21","unstructured":"Gheri, L., Popescu, A.: This Paper\u2019s Homepage. http:\/\/andreipopescu.uk\/papers\/BindingTheory.html"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Gheri, L., Popescu, A.: A formalized general theory of syntax with bindings. CoRR (2017)","DOI":"10.1007\/978-3-319-66107-0_16"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics","author":"AD Gordon","year":"1996","unstructured":"Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 173\u2013190. Springer, Heidelberg (1996). doi:10.1007\/BFb0105404"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Gunter, E.L., Osborn, C.J., Popescu, A.: Theory support for weak higher order abstract syntax in Isabelle\/HOL. In: LFMTP, pp. 12\u201320 (2009)","DOI":"10.1145\/1577824.1577827"},{"key":"16_CR25","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: LICS 1987, pp. 194\u2013204. IEEE Computer Society Press (1987)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","volume-title":"Automata, Languages and Programming","author":"M Hennessy","year":"1980","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: Bakker, J., Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299\u2013309. Springer, Heidelberg (1980). doi:10.1007\/3-540-10003-2_79"},{"issue":"3","key":"16_CR27","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s10817-010-9207-9","volume":"49","author":"A Hirschowitz","year":"2012","unstructured":"Hirschowitz, A., Maggesi, M.: Nested abstract syntax in Coq. J. Autom. Reason. 49(3), 409\u2013426 (2012)","journal-title":"J. Autom. Reason."},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013165. Springer, Heidelberg (1999). doi:10.1007\/3-540-48256-3_11"},{"key":"16_CR29","volume-title":"Model Theory for Infinitary Logic","author":"HJ Keisler","year":"1971","unstructured":"Keisler, H.J.: Model Theory for Infinitary Logic. North-Holland, Amsterdam (1971)"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-642-28869-2_25","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2012","unstructured":"Lochbihler, A.: Java and the Java memory model \u2014 a unified, machine-checked formalisation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 497\u2013517. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28869-2_25"},{"key":"16_CR31","unstructured":"Luttik, B.: Choice quantification in process algebra. Ph.D. thesis, University of Amsterdam, April 2002"},{"issue":"4","key":"16_CR32","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"key":"16_CR33","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"16_CR34","volume-title":"Communicating and Mobile Systems: The $$\\pi $$-Calculus","author":"R Milner","year":"2001","unstructured":"Milner, R.: Communicating and Mobile Systems: The $$\\pi $$-Calculus. Cambridge University Press, Cambridge (2001)"},{"key":"16_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-10542-0"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow, T., von Oheimb, D.: Java$${}_{\\text{light}}$$ is type-safe - definitely. In: POPL, pp. 161\u2013170 (1998)","DOI":"10.1145\/268946.268960"},{"key":"16_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). doi:10.1007\/3-540-45949-9"},{"issue":"2\u20133","key":"16_CR38","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s10990-006-8745-7","volume":"19","author":"M Norrish","year":"2006","unstructured":"Norrish, M.: Mechanising lambda-calculus using a classical first order theory of terms with permutations. High.-Order Symb. Comput. 19(2\u20133), 169\u2013195 (2006)","journal-title":"High.-Order Symb. Comput."},{"key":"16_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-74591-4_16","volume-title":"Theorem Proving in Higher Order Logics","author":"M Norrish","year":"2007","unstructured":"Norrish, M., Vestergaard, R.: Proof pearl: de bruijn terms really do work. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 207\u2013222. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-74591-4_16"},{"key":"16_CR40","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":"AM 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. 2215, pp. 219\u2013242. Springer, Heidelberg (2001). doi:10.1007\/3-540-45500-0_11"},{"issue":"3","key":"16_CR41","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"AM Pitts","year":"2006","unstructured":"Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53(3), 459\u2013506 (2006)","journal-title":"J. ACM"},{"key":"16_CR42","unstructured":"Popescu, A.: Contributions to the theory of syntax with bindings and to process algebra. Ph.D. thesis, University of Illinois (2010). andreipopescu.uk\/thesis.pdf"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-12032-9_9","volume-title":"Foundations of Software Science and Computational Structures","author":"A Popescu","year":"2010","unstructured":"Popescu, A., Gunter, E.L.: Incremental pattern-based coinduction for process algebra and its isabelle formalization. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 109\u2013127. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12032-9_9"},{"key":"16_CR44","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: ICFP, pp. 346\u2013358 (2011)","DOI":"10.1145\/2034574.2034819"},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L., Osborn, C.J.: Strong normalization of system F by HOAS on top of FOAS. In: LICS, pp. 31\u201340 (2010)","DOI":"10.1109\/LICS.2010.48"},{"key":"16_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-35308-6_11","volume-title":"Certified Programs and Proofs","author":"A Popescu","year":"2012","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Proving concurrent noninterference. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 109\u2013125. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-35308-6_11"},{"key":"16_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-319-03545-1_17","volume-title":"Certified Programs and Proofs","author":"A Popescu","year":"2013","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 259\u2013275. Springer, Cham (2013). doi:10.1007\/978-3-319-03545-1_17"},{"key":"16_CR48","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2015.01.047","volume":"577","author":"A Popescu","year":"2015","unstructured":"Popescu, A., Rosu, G.: Term-generic logic. Theor. Comput. Sci. 577, 1\u201324 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-03545-1_8","volume-title":"Certified Programs and Proofs","author":"A Schropp","year":"2013","unstructured":"Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 114\u2013130. Springer, Cham (2013). doi:10.1007\/978-3-319-03545-1_8"},{"issue":"1","key":"16_CR50","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(1), 71\u2013122 (2010)","journal-title":"J. Funct. Program."},{"key":"16_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-71067-7_6"},{"issue":"1\u20132","key":"16_CR52","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0304-3975(97)00170-9","volume":"211","author":"Y Sun","year":"1999","unstructured":"Sun, Y.: An algebraic generalization of frege structures\u2013binding algebras. Theor. Comput. Sci. 211(1\u20132), 189\u2013232 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR53","doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In: LICS 2012, pp. 596\u2013605. IEEE (2012)","DOI":"10.1109\/LICS.2012.75"},{"issue":"4","key":"16_CR54","doi-asserted-by":"publisher","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":"16_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-73595-3_4","volume-title":"Automated Deduction \u2013 CADE-21","author":"C Urban","year":"2007","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s variable convention in rule inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 35\u201350. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-73595-3_4"},{"key":"16_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-19718-5_25","volume-title":"Programming Languages and Systems","author":"C Urban","year":"2011","unstructured":"Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal Isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 480\u2013500. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19718-5_25"},{"key":"16_CR57","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38\u201353. Springer, Heidelberg (2005). doi:10.1007\/11532231_4"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:39:01Z","timestamp":1750808341000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}