{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T14:46:43Z","timestamp":1776350803379,"version":"3.51.2"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"name":"UKRI Future Leaders Fellowship","award":["MR\/S035540\/1"],"award-info":[{"award-number":["MR\/S035540\/1"]}]},{"name":"Wallenberg Academy Fellowship Prolongation project","award":["251080003"],"award-info":[{"award-number":["251080003"]}]},{"name":"VR starting grant","award":["251088801"],"award-info":[{"award-number":["251088801"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,4,30]]},"abstract":"<jats:p>\n                    <jats:italic toggle=\"yes\">Circular<\/jats:italic>\n                    (or\n                    <jats:italic toggle=\"yes\">cyclic<\/jats:italic>\n                    ) proofs have received increasing attention in recent years and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common \u2018recursion schemes\u2019.\n                  <\/jats:p>\n                  <jats:p>\n                    This article attempts to bridge the gap between circular proofs and\n                    <jats:italic toggle=\"yes\">implicit computational complexity<\/jats:italic>\n                    (ICC). Namely, we introduce a circular proof system based on Bellantoni and Cook\u2019s famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way, we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.\n                  <\/jats:p>","DOI":"10.1145\/3793666","type":"journal-article","created":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T12:17:32Z","timestamp":1769861852000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Cyclic Implicit Complexity"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8746-1704","authenticated-orcid":false,"given":"Gianluca","family":"Curzi","sequence":"first","affiliation":[{"name":"Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0142-3676","authenticated-orcid":false,"given":"Anupam","family":"Das","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2024.8"},{"key":"e_1_3_3_3_2","unstructured":"David Baelde Amina Doumane Denis Kuperberg and Alexis Saurin. 2020. Bouncing threads for infinitary and circular proofs. arXiv:2005.08257. Retrieved from https:\/\/arxiv.org\/abs\/2005.08257"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.42"},{"key":"e_1_3_3_5_2","unstructured":"Stephen Bellantoni. 1992. Predicative Recursion and Computational Complexity. PhD thesis."},{"key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-1-4612-2566-9_2","volume-title":"Feasible Mathematics II","author":"Bellantoni Stephen","year":"1995","unstructured":"Stephen Bellantoni. 1995. Predicative recursion and the polytime hierarchy. In Feasible Mathematics II. Peter Clote and Jeffrey B. Remmel (Eds.), Birkh\u00e4user Boston, 15\u201329."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129740"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00006-3"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005114"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_8"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533340"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2023.16"},{"key":"e_1_3_3_14_2","unstructured":"Das Anupam. 2020. A circular version of G\u00f6del\u2019s T and its abstraction complexity. arXiv:2012.14421. Retrieved from https:\/\/arxiv.org\/abs\/2012.14421"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:1)2020"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.29"},{"key":"e_1_3_3_17_2","first-page":"261","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","author":"Das Anupam","year":"2017","unstructured":"Anupam Das and Damien Pous. 2017. A cut-free cyclic proof system for kleene algebra. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Springer, 261\u2013277."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.19"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_3_20_2","first-page":"273","volume-title":"Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Dax Christian","year":"2006","unstructured":"Christian Dax, Martin Hofmann, and Martin Lange. 2006. A proof system for the linear time \\(\\mu\\) -calculus. In Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 273\u2013284."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_17"},{"key":"e_1_3_3_22_2","volume-title":"Proceedings of the Computer Science Logic 2013 (CSL \u201913)","author":"Fortier J\u00e9r\u00f4me","year":"2013","unstructured":"J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for circular proofs: Semantics and cut-elimination. In Proceedings of the Computer Science Logic 2013 (CSL \u201913), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028020"},{"key":"e_1_3_3_24_2","volume-title":"Introduction to Metamathematics (7 ed.)","author":"Cole Kleene Stephen","year":"1971","unstructured":"Stephen Cole Kleene. 1971. Introduction to Metamathematics (7 ed.). Wolters-Noordhoff Publishing."},{"issue":"2","key":"e_1_3_3_25_2","first-page":"16:1","article-title":"The logical strength of B\u00fcchi\u2019s decidability theorem","volume":"15","author":"Kolodziejczyk Leszek Aleksander","year":"2019","unstructured":"Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. 2019. The logical strength of B\u00fcchi\u2019s decidability theorem. Logical Methods in Computer Science 15, 2 (2019), 16:1\u201316:31. https:\/\/doi.org\/10.23638\/LMCS-15(2:16)2019","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434282"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151625"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00040-2"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022277"},{"issue":"4","key":"e_1_3_3_30_2","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/BF01091743","article-title":"Finite investigations of transfinite derivations","volume":"10","author":"Mints Grigori E.","year":"1978","unstructured":"Grigori E. Mints. 1978. Finite investigations of transfinite derivations. Journal of Soviet Mathematics 10, 4 (1978), 548\u2013596.","journal-title":"Journal of Soviet Mathematics"},{"issue":"1","key":"e_1_3_3_31_2","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","article-title":"Games for the  \\(\\mu\\) -calculus","volume":"163","author":"Niwi\u0144ski Damian","year":"1996","unstructured":"Damian Niwi\u0144ski and Igor Walukiewicz. 1996. Games for the \\(\\mu\\) -calculus. Theoretical Computer Science 163, 1\u20132 (1996), 99\u2013116.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610056"},{"key":"e_1_3_3_34_2","volume-title":"Subrecursion: Functions and Hierarchies","author":"Rose H. E.","year":"1984","unstructured":"H. E. Rose. 1984. Subrecursion: Functions and Hierarchies. Oxford University Press."},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"e_1_3_3_36_2","unstructured":"Marc Wirz. 1999. Characterizing the Grzegorczyk Hierarchy by Safe Recursion. Universit\u00e4t Bern."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3793666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T13:51:42Z","timestamp":1776347502000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3793666"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,16]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3793666"],"URL":"https:\/\/doi.org\/10.1145\/3793666","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,16]]},"assertion":[{"value":"2024-04-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-10","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}