{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:40:13Z","timestamp":1758667213018,"version":"3.44.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,11]],"date-time":"2025-08-11T00:00:00Z","timestamp":1754870400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,11]],"date-time":"2025-08-11T00:00:00Z","timestamp":1754870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Reasoning about substitution remains one of the most tedious and error-prone aspects of formal metatheory. We present Tealeaves, a framework implemented in Coq for developing such infrastructure generically and modularly. Tealeaves is centered on a novel categorical abstraction, decorated traversable monads (DTMs), which provide a unifying foundation for first-order syntax and enable local, compositional reasoning about syntactic operations, such as substitution, that are defined purely by their effect on individual variable occurrences. Within this framework, Tealeaves supports extensible backend modules, each implementing the metatheory of a specific concrete strategy for representing binders. Our current backends include implementations of de Bruijn indices in the style of Autosubst, as well as locally nameless in the style of LNgen. Tealeaves goes further by providing a certified translation between these representations, illustrating how DTMs reconcile their underlying structures. The framework also accommodates challenging features such as variadic and mutually-recursive binders, which are often overlooked by both theoretical treatments and practical tools. We describe the implementation and use of Tealeaves\u2019 backends in formalized language developments, introduce the equational axioms that characterize DTMs, and conclude with a presentation of those axioms instantiated for the lambda calculus extended with a variadic binding constructor.<\/jats:p>","DOI":"10.1007\/s10817-025-09731-y","type":"journal-article","created":{"date-parts":[[2025,8,11]],"date-time":"2025-08-11T10:04:24Z","timestamp":1754906664000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Structured Monads for Generic First-Order Syntax Metatheory"],"prefix":"10.1007","volume":"69","author":[{"given":"Lawrence","family":"Dunn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Val","family":"Tannen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,11]]},"reference":[{"key":"9731_CR1","doi-asserted-by":"publisher","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics. TPHOLs \u201905, pp. 50\u201365. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_4","DOI":"10.1007\/11541868_4"},{"key":"9731_CR2","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201914, pp. 179\u2013191. Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"9731_CR3","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2(POPL) (2017) https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"9731_CR4","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. SOSP \u201909, pp. 207\u2013220. Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"issue":"10","key":"9731_CR5","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/3356903","volume":"62","author":"R Gu","year":"2019","unstructured":"Gu, R., Shao, Z., Chen, H., Kim, J., Koenig, J., Wu, X.N., Sj\u00f6berg, V., Costanzo, D.: Building certified concurrent OS kernels. Commun. ACM 62(10), 89\u201399 (2019). https:\/\/doi.org\/10.1145\/3356903","journal-title":"Commun. ACM"},{"key":"9731_CR6","unstructured":"The Coq Development Team: The Coq Reference Manual \u2013 Release 8.19.0. https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman (2024)"},{"issue":"2\u20133","key":"9731_CR7","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(94)00022-0","volume":"23","author":"F Bellegarde","year":"1994","unstructured":"Bellegarde, F., Hook, J.: Substitution: A formal methods case study using monads and transformations. Sci. Comput. Program. 23(2\u20133), 287\u2013311 (1994). https:\/\/doi.org\/10.1016\/0167-6423(94)00022-0","journal-title":"Sci. Comput. Program."},{"key":"9731_CR8","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) Computer Science Logic, 13th International Workshop, CSL \u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings. Lec. Notes Comput. Sci., vol. 1683, pp. 453\u2013468. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48168-0_32","DOI":"10.1007\/3-540-48168-0_32"},{"issue":"1","key":"9731_CR9","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). https:\/\/doi.org\/10.1017\/s0956796899003366","journal-title":"J. Funct. Program."},{"key":"9731_CR10","doi-asserted-by":"publisher","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pp. 193\u2013202. IEEE Computer Society, USA (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782615","DOI":"10.1109\/LICS.1999.782615"},{"key":"9731_CR11","doi-asserted-by":"publisher","unstructured":"Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science. LICS \u201908, pp. 57\u201368. IEEE Computer Society, USA (2008). https:\/\/doi.org\/10.1109\/LICS.2008.38","DOI":"10.1109\/LICS.2008.38"},{"key":"9731_CR12","doi-asserted-by":"publisher","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. Journal of Functional Programming 31, 22 (2021) https:\/\/doi.org\/10.1017\/S0956796820000076","DOI":"10.1017\/S0956796820000076"},{"key":"9731_CR13","doi-asserted-by":"publisher","unstructured":"Fiore, M., Szamozvancev, D.: Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang. 6(POPL) (2022) https:\/\/doi.org\/10.1145\/3498715","DOI":"10.1145\/3498715"},{"key":"9731_CR14","doi-asserted-by":"publisher","unstructured":"Ahrens, B., Matthes, R., M\u00f6rtberg, A.: Implementing a category-theoretic framework for typed abstract syntax. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022, pp. 307\u2013323. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503678","DOI":"10.1145\/3497775.3503678"},{"issue":"5","key":"9731_CR15","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381\u2013392 (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"9731_CR16","doi-asserted-by":"publisher","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 of Programming Languages. POPL \u201908, pp. 3\u201315. Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1328438.1328443","DOI":"10.1145\/1328438.1328443"},{"key":"9731_CR17","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, S., Tebbi, T., Smolka, G.: Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In: Zhang, X., Urban, C. (eds.) Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015. LNAI. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_24","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"9731_CR18","unstructured":"Aydemir, B., Weirich, S.: LNgen: Tool Support for Locally Nameless Representations. Technical report, University of Pennsylvania, Department of Computer and Information Science (June 2010). https:\/\/repository.upenn.edu\/cis_reports\/933\/"},{"issue":"12","key":"9731_CR19","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/2578854.2503781","volume":"48","author":"R Bird","year":"2013","unstructured":"Bird, R., Gibbons, J., Mehner, S., Voigtl\u00e4nder, J., Schrijvers, T.: Understanding idiomatic traversals backwards and forwards. ACM SIGPLAN Not. 48(12), 25\u201336 (2013). https:\/\/doi.org\/10.1145\/2578854.2503781","journal-title":"ACM SIGPLAN Not."},{"key":"9731_CR20","doi-asserted-by":"publisher","unstructured":"Jaskelioff, M., O\u2019Connor, R.: A representation theorem for second-order functionals. Journal of Functional Programming 25 (2014) https:\/\/doi.org\/10.1017\/S0956796815000088","DOI":"10.1017\/S0956796815000088"},{"issue":"3\u20135","key":"9731_CR21","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"MJ Gabbay","year":"2002","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13(3\u20135), 341\u2013363 (2002). https:\/\/doi.org\/10.1007\/s001650200016","journal-title":"Form. Asp. Comput."},{"issue":"2","key":"9731_CR22","doi-asserted-by":"publisher","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. Information and Computation 186(2), 165\u2013193 (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00138-X. (Theoretical Aspects of Computer Software (TACS 2001))","journal-title":"Information and Computation"},{"key":"9731_CR23","doi-asserted-by":"publisher","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20, pp. 38\u201353. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_4","DOI":"10.1007\/11532231_4"},{"key":"9731_CR24","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) Proceedings of the ACM SIGPLAN\u201988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, pp. 199\u2013208. ACM, New York, NY, USA (1988). https:\/\/doi.org\/10.1145\/53990.54010","DOI":"10.1145\/53990.54010"},{"key":"9731_CR25","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. ICFP \u201908, pp. 143\u2013156. Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1411204.1411226","DOI":"10.1145\/1411204.1411226"},{"key":"9731_CR26","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15232965","author":"L Dunn","year":"2025","unstructured":"Dunn, L.: Tealeaves. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15232965","journal-title":"Tealeaves. Zenodo"},{"key":"9731_CR27","doi-asserted-by":"publisher","unstructured":"Dunn, L., Tannen, V., Zdancewic, S.: Tealeaves: Structured monads for generic first-order abstract syntax infrastructure. In: International Conference on Interactive Theorem Proving (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.14","DOI":"10.4230\/LIPIcs.ITP.2023.14"},{"issue":"4","key":"9731_CR28","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375\u2013416 (1991). https:\/\/doi.org\/10.1017\/S0956796800000186","journal-title":"Journal of Functional Programming"},{"key":"9731_CR29","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, S., Smolka, G., Tebbi, T.: Completeness and decidability of de Bruijn substitution algebra in coq. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. CPP \u201915, pp. 67\u201373. Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676724.2693163","DOI":"10.1145\/2676724.2693163"},{"key":"9731_CR30","doi-asserted-by":"publisher","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: Reasoning with multi-sorted de Bruijn terms and vector substitutions. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2019, pp. 166\u2013180. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3293880.3294101","DOI":"10.1145\/3293880.3294101"},{"issue":"3","key":"9731_CR31","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). https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"J. Autom. Reason."},{"key":"9731_CR32","doi-asserted-by":"publisher","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strni\u0161a, R.: Ott: Effective tool support for the working semanticist. In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming. ICFP \u201907, pp. 1\u201312. Association for Computing Machinery, New York, NY, USA (2007). https:\/\/doi.org\/10.1145\/1291151.1291155","DOI":"10.1145\/1291151.1291155"},{"key":"9731_CR33","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics. TPHOLs \u201908, pp. 278\u2013293. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"9731_CR34","doi-asserted-by":"publisher","unstructured":"Spitters, B., Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21 (2011) https:\/\/doi.org\/10.1017\/S0960129511000119","DOI":"10.1017\/S0960129511000119"},{"issue":"1","key":"9731_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796807006326","volume":"18","author":"C McBride","year":"2008","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1\u201313 (2008). https:\/\/doi.org\/10.1017\/S0956796807006326","journal-title":"J. Funct. Program."},{"key":"9731_CR36","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Computational lambda-calculus and monads. Proceedings. Fourth Annual Symposium on Logic in Computer Science, 14\u201323 (1989) https:\/\/doi.org\/10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"9731_CR37","doi-asserted-by":"publisher","unstructured":"Wadler, P.: The essence of functional programming. In: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201992, pp. 1\u201314. Association for Computing Machinery, New York, NY, USA (1992). https:\/\/doi.org\/10.1145\/143165.143169","DOI":"10.1145\/143165.143169"},{"key":"9731_CR38","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-31113-0_15","volume-title":"Mathematics of Program Construction","author":"R Paterson","year":"2012","unstructured":"Paterson, R.: Constructing applicative functors. In: Gibbons, J., Nogueira, P. (eds.) Mathematics of Program Construction, pp. 300\u2013323. Springer, Berlin, Heidelberg (2012)"},{"key":"9731_CR39","doi-asserted-by":"publisher","unstructured":"Dunn, L., Tannen, V., Zdancewic, S.: Syntax monads for the working formal metatheorist. Electronic Proceedings in Theoretical Computer Science 397, 98\u2013117 (2023) https:\/\/doi.org\/10.4204\/EPTCS.397.7","DOI":"10.4204\/EPTCS.397.7"},{"key":"9731_CR40","volume-title":"Foundations of Databases: The Logical Level","author":"S Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: The Logical Level, 1st edn. Addison-Wesley Longman Publishing Co., Inc, USA (1995)","edition":"1"},{"key":"9731_CR41","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, Cambridge, MA (2013)"},{"key":"9731_CR42","doi-asserted-by":"publisher","unstructured":"Jay, C.B., Cockett, J.R.B.: Shapely types and shape polymorphism. In: Sannella, D. (ed.) Programming Languages and Systems \u2014 ESOP \u201994, pp. 302\u2013316. Springer, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57880-3_20","DOI":"10.1007\/3-540-57880-3_20"},{"key":"9731_CR43","doi-asserted-by":"publisher","unstructured":"Capriotti, P., Kaposi, A.: Free applicative functors. Electronic Proceedings in Theoretical Computer Science 153 (2014) https:\/\/doi.org\/10.4204\/EPTCS.153.2","DOI":"10.4204\/EPTCS.153.2"},{"key":"9731_CR44","doi-asserted-by":"publisher","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings. Lec. Notes Comput. Sci., vol. 1955, pp. 85\u201395. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7","DOI":"10.1007\/3-540-44404-1_7"},{"key":"9731_CR45","doi-asserted-by":"publisher","unstructured":"Lee, G., Oliveira, B.C.D.S., Cho, S., Yi, K.: GMeta: A generic formal metatheory framework for first-order representations. In: Seidl, H. (ed.) Programming Languages and Systems. Lec. Notes Comput. Sci., vol. 7211, pp. 436\u2013455. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_22","DOI":"10.1007\/978-3-642-28869-2_22"},{"key":"9731_CR46","first-page":"1","volume-title":"Datatype-Generic Programming","author":"J Gibbons","year":"2007","unstructured":"Gibbons, J.: Datatype-generic programming. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) Datatype-Generic Programming, pp. 1\u201371. Springer, Berlin, Heidelberg (2007)"},{"key":"9731_CR47","unstructured":"Pottier, F., Coq maintainers: dblib. GitHub (2013). https:\/\/github.com\/coq-community\/dblib"},{"key":"9731_CR48","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0054285","volume":"1422","author":"R Bird","year":"1998","unstructured":"Bird, R., Meertens, L.: Nested datatypes. 1422, 52\u201367 (1998). https:\/\/doi.org\/10.1007\/BFb0054285","journal-title":"Nested datatypes."},{"key":"9731_CR49","doi-asserted-by":"publisher","unstructured":"Hirschowitz, A., Hirschowitz, T., Lafont, A., Maggesi, M.: Variable binding and substitution for (nameless) dummies. In: Bouyer, P., Schr\u00f6der, L. (eds.) Foundations of Software Science and Computation Structures, pp. 389\u2013408. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_20","DOI":"10.1007\/978-3-030-99253-8_20"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09731-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09731-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09731-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:33Z","timestamp":1758664953000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09731-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,11]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9731"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09731-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,8,11]]},"assertion":[{"value":"18 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"22"}}