{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:50:37Z","timestamp":1770292237756,"version":"3.49.0"},"reference-count":112,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T00:00:00Z","timestamp":1555372800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N019547\/1"],"award-info":[{"award-number":["EP\/N019547\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"UK Research Institute in Verified Trustworthy Software Systems"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s10817-019-09522-2","type":"journal-article","created":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T04:42:24Z","timestamp":1555389744000},"page":"641-675","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Formalized General Theory of Syntax with Bindings: Extended Version"],"prefix":"10.1007","volume":"64","author":[{"given":"Lorenzo","family":"Gheri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8747-0619","authenticated-orcid":false,"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,16]]},"reference":[{"key":"9522_CR1","unstructured":"Abel, A., Momigliano, A., Pientka, B.: POPLMark Reloaded. In: LFMTP (2017)"},{"key":"9522_CR2","doi-asserted-by":"crossref","unstructured":"Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type and scope safe universe of syntaxes with binding: their semantics and proofs. In: PACMPL 2(ICFP), pp. 90:1\u201390:30 (2018)","DOI":"10.1145\/3236785"},{"key":"9522_CR3","doi-asserted-by":"crossref","unstructured":"Allais, G., Chapman, J., McBride, C., McKinna, J.: Type-and-scope safe programs and their proofs. In: CPP, pp. 195\u2013207 (2017)","DOI":"10.1145\/3018610.3018613"},{"key":"9522_CR4","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. J. Funct. Program. 25, (2015)","DOI":"10.1017\/S095679681500009X"},{"key":"9522_CR5","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: CSL, pp. 453\u2013468 (1999)","DOI":"10.1007\/3-540-48168-0_32"},{"key":"9522_CR6","unstructured":"Aydemir, B., Weirich, S.: LNgen: Tool support for locally nameless representations. Tech. rep., UPenn (2010)"},{"issue":"5","key":"9522_CR7","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). Electr. Notes Theor. Comput. Sci. 174(5), 69\u201377 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9522_CR8","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL, pp. 3\u201315 (2008)","DOI":"10.1145\/1328897.1328443"},{"issue":"2","key":"9522_CR9","first-page":"1","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reason. 7(2), 1\u201389 (2014)","journal-title":"J. Formalized Reason."},{"key":"9522_CR10","volume-title":"The Lambda Calculus","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus. North-Holland, Amsterdam (1984)"},{"key":"9522_CR11","doi-asserted-by":"crossref","unstructured":"Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: CPP, pp. 164\u2013172 (2017)","DOI":"10.1145\/3018610.3018615"},{"issue":"1","key":"9522_CR12","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."},{"issue":"5","key":"9522_CR13","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2007.01.018","volume":"174","author":"S Berghofer","year":"2007","unstructured":"Berghofer, S., Urban, C.: A head-to-head comparison of De Bruijn indices and names. Electr. Notes Theor. Comput. Sci. 174(5), 53\u201367 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9522_CR14","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL\u2014Lessons learned in formal-logic engineering. In: TPHOLs, pp. 19\u201336 (1999)","DOI":"10.1007\/3-540-48256-3_3"},{"issue":"1","key":"9522_CR15","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"RS Bird","year":"1999","unstructured":"Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. J. Funct. Program 9(1), 77\u201391 (1999)","journal-title":"J. Funct. Program"},{"key":"9522_CR16","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: TACAS, pp. 493\u2013507 (2013)","DOI":"10.1007\/978-3-642-36742-7_34"},{"key":"9522_CR17","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. \nhttps:\/\/doi.org\/10.2168\/LMCS-2014-1018","DOI":"10.2168\/LMCS-2014-1018"},{"key":"9522_CR18","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits\u2013implementing corecursion in foundational proof assistants. In: ESOP, pp. 111\u2013140 (2017)","DOI":"10.1007\/978-3-662-54434-1_5"},{"key":"9522_CR19","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Gheri, L., Popescu, A., Traytel, D.: Bindings as bounded natural functors. In: PACMPL 3(POPL), pp. 22:1\u201322:34 (2019)","DOI":"10.1145\/3290335"},{"key":"9522_CR20","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: ITP, pp. 93\u2013110 (2014)","DOI":"10.1007\/978-3-319-08970-6_7"},{"key":"9522_CR21","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: LICS, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005071"},{"key":"9522_CR22","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: FroCoS, pp. 245\u2013260 (2013)","DOI":"10.1007\/978-3-642-40885-4_17"},{"key":"9522_CR23","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle\/HOL. In: ITP, pp. 111\u2013127 (2014)","DOI":"10.1007\/978-3-319-08970-6_8"},{"key":"9522_CR24","first-page":"46","volume":"2014","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness\u2013a coinductive pearl. IJCAR 2014, 46\u201360 (2014)","journal-title":"IJCAR"},{"key":"9522_CR25","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":"9522_CR26","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."},{"issue":"5","key":"9522_CR27","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N Bruijn de","year":"1972","unstructured":"de Bruijn, N.: \n$$\\lambda $$\n\n\n\n\u03bb\n\n\n\n-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church\u2013Rosser theorem. Indag. Math 34(5), 381\u2013392 (1972)","journal-title":"Indag. Math"},{"issue":"3","key":"9522_CR28","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363\u2013408 (2012)","journal-title":"J. Autom. Reason."},{"key":"9522_CR29","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"},{"issue":"2","key":"9522_CR30","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"9522_CR31","doi-asserted-by":"crossref","unstructured":"Copello, E., Szasz, N., Tasistro, \u00c1.: Formalisation in constructive type theory of Barendregt\u2019s variable convention for generic structures with binders. In: LFMTP, pp. 11\u201326 (2018)","DOI":"10.4204\/EPTCS.274.2"},{"issue":"1\u20133","key":"9522_CR32","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/S0019-9958(86)80047-X","volume":"69","author":"PL Curien","year":"1986","unstructured":"Curien, P.L.: Categorical combinators. Inf. Control 69(1\u20133), 188\u2013254 (1986)","journal-title":"Inf. Control"},{"key":"9522_CR33","doi-asserted-by":"crossref","unstructured":"Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: TLCA, pp. 124\u2013138 (1995)","DOI":"10.1007\/BFb0014049"},{"key":"9522_CR34","unstructured":"van Doorn, F.: On the formalization of higher inductive types and synthetic homotopy theory. Ph.D. thesis, Carnegie Mellon University (2018)"},{"issue":"1","key":"9522_CR35","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":"9522_CR36","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Momigliano, A., Pientka, B.: An open challenge problem repository for systems supporting binders. In: LFMTP, pp. 18\u201332 (2015)","DOI":"10.4204\/EPTCS.185.2"},{"key":"9522_CR37","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Pientka, B.: Reasoning with higher-order abstract syntax and contexts: a comparison. In: ITP, pp. 227\u2013242 (2010)","DOI":"10.1007\/978-3-642-14052-5_17"},{"key":"9522_CR38","doi-asserted-by":"crossref","unstructured":"Ferreira, F., Pientka, B.: Programs using syntax with first-class binders. In: ESOP, pp. 504\u2013529 (2017)","DOI":"10.1007\/978-3-662-54434-1_19"},{"key":"9522_CR39","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1112\/jlms\/jdm096","volume":"1","author":"M Fiore","year":"2008","unstructured":"Fiore, M., Gambino, N., Hyland, M., Winskel, G.: The cartesian closed bicategory of generalised species of structures. J. London Math. Soc. 1, 203\u2013220 (2008)","journal-title":"J. London Math. Soc."},{"key":"9522_CR40","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding (extended abstract). In: LICS, pp. 193\u2013202 (1999)"},{"key":"9522_CR41","unstructured":"Gabbay, M., Pitts, A.M.: A new approach to abstract syntax involving binders. In: LICS, pp. 214\u2013224 (1999)"},{"issue":"3\u20135","key":"9522_CR42","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M Gabbay","year":"2002","unstructured":"Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3\u20135), 341\u2013363 (2002)","journal-title":"Formal Asp. Comput."},{"issue":"7","key":"9522_CR43","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":"9522_CR44","doi-asserted-by":"crossref","unstructured":"Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: TYPES, pp. 210\u2013225 (2003)","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"9522_CR45","unstructured":"Gheri, L., Popescu, A.: A case study in reasoning about syntax with bindings: the Church\u2013Rosser and standardization theorems. Submitted to the Journal of Automated Reasoning. \nhttp:\/\/andreipopescu.uk\/papers\/cbncbv.pdf"},{"key":"9522_CR46","unstructured":"Gheri, L., Popescu, A.: A general theory of syntax with bindings. Arch. Form. Proofs. (2019). \nhttp:\/\/isa-afp.org\/entries\/Binding_Syntax_Theory.html"},{"key":"9522_CR47","doi-asserted-by":"crossref","unstructured":"Gheri, L., Popescu, A.: A formalized general theory of syntax with bindings. In: ITP (2017)","DOI":"10.1007\/978-3-319-66107-0_16"},{"key":"9522_CR48","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Melham, T.F.: Five axioms of alpha-conversion. In: TPHOLs, pp. 173\u2013190 (1996)","DOI":"10.1007\/BFb0105404"},{"key":"9522_CR49","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":"9522_CR50","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: LICS, pp. 194\u2013204 (1987)"},{"key":"9522_CR51","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: IJCAR, pp. 177\u2013191 (2006)","DOI":"10.1007\/11814771_17"},{"key":"9522_CR52","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: ICALP, pp. 299\u2013309 (1980)","DOI":"10.1007\/3-540-10003-2_79"},{"key":"9522_CR53","unstructured":"Hinze, R.: Polytypic programming with ease. J. Funct. Logic Program. 2001(3) (2001)"},{"issue":"5","key":"9522_CR54","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1016\/j.ic.2009.07.003","volume":"208","author":"A Hirschowitz","year":"2010","unstructured":"Hirschowitz, A., Maggesi, M.: Modules over monads and initial semantics. Inf. Comput. 208(5), 545\u2013564 (2010)","journal-title":"Inf. Comput."},{"key":"9522_CR55","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: LICS (1999)"},{"key":"9522_CR56","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"GP Huet","year":"1978","unstructured":"Huet, G.P., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Inf. 11, 31\u201355 (1978). \nhttps:\/\/doi.org\/10.1007\/BF00264598","journal-title":"Acta Inf."},{"key":"9522_CR57","unstructured":"IsaFoL (Isabelle Formalization of Logic) project (2018). \nhttps:\/\/bitbucket.org\/isafol\/isafol\/wiki\/Home"},{"key":"9522_CR58","unstructured":"Joachimski, F.: Reduction properties of \n$$\\varPi \\text{IE}$$\n\n\n\n\n\u03a0\nIE\n\n\n\n\n-systems. Ph.D. thesis, LMU M\u00fcnchen (2001)"},{"key":"9522_CR59","doi-asserted-by":"crossref","unstructured":"Kaiser, J., Sch\u00e4fer, S., Stark, K.: Binder aware recursion over well-scoped De Bruijn syntax. In: CPP, pp. 293\u2013306 (2018)","DOI":"10.1145\/3176245.3167098"},{"key":"9522_CR60","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014a sectioning concept for Isabelle. In: TPHOLs, pp. 149\u2013166 (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9522_CR61","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":"9522_CR62","doi-asserted-by":"crossref","unstructured":"Keuchel, S., Jeuring, J.: Generic conversions of abstract syntax representations. In: Workshop on Generic Programming, pp. 57\u201368 (2012)","DOI":"10.1145\/2364394.2364403"},{"key":"9522_CR63","doi-asserted-by":"crossref","unstructured":"Keuchel, S., Weirich, S., Schrijvers, T.: Needle & Knot: Binder boilerplate tied up. In: ESOP, pp. 419\u2013445 (2016)","DOI":"10.1007\/978-3-662-49498-1_17"},{"key":"9522_CR64","doi-asserted-by":"crossref","unstructured":"Lee, G., Oliveira, B.C., Cho, S., Yi, K.: GMeta: a generic formal metatheory framework for first-order representations. In: ESOP, pp. 436\u2013455 (2012)","DOI":"10.1007\/978-3-642-28869-2_22"},{"key":"9522_CR65","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Harper, R.: A universe of binding and computation. In: ICFP \u201909, pp. 123\u2013134 (2009)","DOI":"10.1145\/1631687.1596571"},{"key":"9522_CR66","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Java and the Java memory model\u2014a unified, machine-checked formalisation. In: H. Seidl (ed.) ESOP 2012, LNCS, vol. 7211, pp. 497\u2013517. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28869-2_25"},{"key":"9522_CR67","unstructured":"Luttik, B.: Choice quantification in process algebra. Ph.D. thesis, University of Amsterdam (2002)"},{"issue":"4","key":"9522_CR68","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":"9522_CR69","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)"},{"key":"9522_CR70","volume-title":"Communicating and Mobile Systems: The $$\\pi $$ \u03c0 -calculus","author":"R Milner","year":"2001","unstructured":"Milner, R.: Communicating and Mobile Systems: The \n$$\\pi $$\n\n\n\n\u03c0\n\n\n\n-calculus. Cambridge University Press, Cambridge (2001)"},{"key":"9522_CR71","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, Berlin (2014)"},{"key":"9522_CR72","doi-asserted-by":"crossref","unstructured":"Nipkow, T., von Oheimb, D.: \n$$\\text{ Java }{}_{{\\rm light}}$$\n\n\n\n\n\nJava\n\n\n\nlight\n\n\n\n\n\n is type-safe - definitely. In: POPL, pp. 161\u2013170 (1998)","DOI":"10.1145\/268946.268960"},{"key":"9522_CR73","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, Berlin (2002)"},{"key":"9522_CR74","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press, Oxford (1990)"},{"issue":"2\u20133","key":"9522_CR75","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. Higher-Order Symb. Comput. 19(2\u20133), 169\u2013195 (2006)","journal-title":"Higher-Order Symb. Comput."},{"key":"9522_CR76","doi-asserted-by":"crossref","unstructured":"Norrish, M., Vestergaard, R.: Proof pearl: De Bruijn terms really do work. In: TPHOLs, pp. 207\u2013222 (2007)","DOI":"10.1007\/978-3-540-74591-4_16"},{"issue":"3","key":"9522_CR77","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989)","journal-title":"J. Autom. Reason."},{"key":"9522_CR78","volume-title":"Computation and Deduction","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F.: Computation and Deduction. Cambridge University Press, Cambridge (2001)"},{"key":"9522_CR79","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI, pp. 199\u2013208 (1988)","DOI":"10.1145\/960116.54010"},{"key":"9522_CR80","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI, pp. 199\u2013208 (1988)","DOI":"10.1145\/960116.54010"},{"key":"9522_CR81","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2013A meta-logical framework for deductive systems. In: CADE, pp. 202\u2013206 (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"9522_CR82","doi-asserted-by":"crossref","unstructured":"Pientka, B.: Beluga: Programming with dependent types, contextual data, and contexts. In: FLOPS, pp. 1\u201312 (2010)","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"9522_CR83","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: TACS, pp. 219\u2013242 (2001)","DOI":"10.1007\/3-540-45500-0_11"},{"key":"9522_CR84","doi-asserted-by":"publisher","first-page":"3","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 (2006)","journal-title":"J. ACM"},{"issue":"2","key":"9522_CR85","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"9522_CR86","doi-asserted-by":"crossref","unstructured":"Pollack, R.: Closure under alpha-conversion. In: TYPES, pp. 313\u2013332 (1993)","DOI":"10.1007\/3-540-58085-9_82"},{"issue":"2","key":"9522_CR87","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10817-011-9229-y","volume":"49","author":"R Pollack","year":"2012","unstructured":"Pollack, R., Sato, M., Ricciotti, W.: A canonical locally named representation of binding. J. Autom. Reason. 49(2), 185\u2013207 (2012)","journal-title":"J. Autom. Reason."},{"key":"9522_CR88","doi-asserted-by":"crossref","unstructured":"Polonowski, E.: Automatically generated infrastructure for de Bruijn syntaxes. In: ITP, pp. 402\u2013417 (2013)","DOI":"10.1007\/978-3-642-39634-2_29"},{"key":"9522_CR89","unstructured":"Popescu, A.: Contributions to the theory of syntax with bindings and to process algebra (2010). PhD thesis, Univ. of Illinois"},{"key":"9522_CR90","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L.: Incremental pattern-based coinduction for process algebra and its Isabelle formalization. In: FoSSaCS (2010)","DOI":"10.1007\/978-3-642-12032-9_9"},{"key":"9522_CR91","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":"9522_CR92","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":"9522_CR93","doi-asserted-by":"crossref","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Proving concurrent noninterference. In: CPP, pp. 109\u2013125 (2012)","DOI":"10.1007\/978-3-642-35308-6_11"},{"key":"9522_CR94","doi-asserted-by":"crossref","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: CPP, pp. 259\u2013275 (2013)","DOI":"10.1007\/978-3-319-03545-1_17"},{"key":"9522_CR95","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., Ro\u015fu, G.: Term-generic logic. Theor. Comput. Sci. 577, 1\u201324 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9522_CR96","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2008.12.120","volume":"228","author":"A Poswolsky","year":"2009","unstructured":"Poswolsky, A., Sch\u00fcrmann, C.: System description: Delphin\u2013a functional programming language for deductive systems. Electr. Notes Theor. Comput. Sci. 228, 113\u2013120 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9522_CR97","doi-asserted-by":"crossref","unstructured":"Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: TLDI, pp. 89\u2013102 (2010)","DOI":"10.1145\/1708016.1708028"},{"key":"9522_CR98","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, S., Tebbi, T., Smolka, G.: Autosubst: reasoning with De Bruijn terms and parallel substitutions. In: ITP (2015)","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"9522_CR99","doi-asserted-by":"crossref","unstructured":"Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle\/HOL\u2013animating a many-sorted metatheory. In: CPP, pp. 114\u2013130 (2013)","DOI":"10.1007\/978-3-319-03545-1_8"},{"issue":"1\u20132","key":"9522_CR100","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(00)00418-7","volume":"266","author":"C Schurmann","year":"2001","unstructured":"Schurmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1\u20132), 1\u201357 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9522_CR101","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":"9522_CR102","doi-asserted-by":"crossref","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted De Bruijn terms and vector substitutions. In: CPP (2019). To appear","DOI":"10.1145\/3293880.3294101"},{"key":"9522_CR103","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"59","author":"A Stoughton","year":"1988","unstructured":"Stoughton, A.: Substitution revisited. Theor. Comput. Sci. 59, 317\u2013325 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"9522_CR104","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-binding algebras. Theor. Comput. Sci. 211(1\u20132), 189\u2013232 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9522_CR105","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120\u2013127 (1995)","journal-title":"Inf. Comput."},{"key":"9522_CR106","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, pp. 596\u2013605 (2012)","DOI":"10.1109\/LICS.2012.75"},{"key":"9522_CR107","unstructured":"The POPLmark challenge (2009). \nhttps:\/\/www.seas.upenn.edu\/~plclub\/poplmark\/"},{"issue":"4","key":"9522_CR108","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":"9522_CR109","doi-asserted-by":"crossref","unstructured":"Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle\/HOL. In: IJCAR, pp. 498\u2013512 (2006)","DOI":"10.1007\/11814771_41"},{"key":"9522_CR110","doi-asserted-by":"crossref","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s variable convention in rule inductions. In: CADE, pp. 35\u201350 (2007)","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"9522_CR111","doi-asserted-by":"crossref","unstructured":"Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. In: ESOP, pp. 480\u2013500 (2011)","DOI":"10.1007\/978-3-642-19718-5_25"},{"key":"9522_CR112","doi-asserted-by":"crossref","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. In: CADE, pp. 38\u201353 (2005)","DOI":"10.1007\/11532231_4"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09522-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09522-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09522-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,14]],"date-time":"2020-04-14T23:09:15Z","timestamp":1586905755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09522-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,16]]},"references-count":112,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["9522"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09522-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,16]]},"assertion":[{"value":"27 April 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 April 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 April 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}