{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T07:30:06Z","timestamp":1769931006376,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533340","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Cyclic Implicit Complexity"],"prefix":"10.1145","author":[{"given":"Gianluca","family":"Curzi","sequence":"first","affiliation":[{"name":"University of Birmingham, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anupam","family":"Das","sequence":"additional","affiliation":[{"name":"University of Birmingham, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"David Baelde Amina Doumane Denis Kuperberg and Alexis Saurin. 2020. Bouncing threads for infinitary and circular proofs. CoRR abs\/2005.08257(2020). arXiv:2005.08257https:\/\/arxiv.org\/abs\/2005.08257  David Baelde Amina Doumane Denis Kuperberg and Alexis Saurin. 2020. Bouncing threads for infinitary and circular proofs. CoRR abs\/2005.08257(2020). arXiv:2005.08257https:\/\/arxiv.org\/abs\/2005.08257"},{"key":"e_1_3_2_1_2_1","volume-title":"Infinitary Proof Theory: the Multiplicative Additive Case. 62","author":"Baelde David","year":"2016","unstructured":"David Baelde , Amina Doumane , and Alexis Saurin . 2016. Infinitary Proof Theory: the Multiplicative Additive Case. 62 ( 2016 ), 42:1\u201342:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42 10.4230\/LIPIcs.CSL.2016.42 David Baelde, Amina Doumane, and Alexis Saurin. 2016. Infinitary Proof Theory: the Multiplicative Additive Case. 62 (2016), 42:1\u201342:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42"},{"key":"e_1_3_2_1_4_1","volume-title":"Predicative Recursion and The Polytime Hierarchy","author":"Bellantoni Stephen","unstructured":"Stephen Bellantoni . 1995. Predicative Recursion and The Polytime Hierarchy . In Feasible Mathematics II, Peter Clote and Jeffrey\u00a0B. Remmel (Eds.). Birkh\u00e4user Boston , Boston, MA , 15\u201329. Stephen Bellantoni. 1995. Predicative Recursion and The Polytime Hierarchy. In Feasible Mathematics II, Peter Clote and Jeffrey\u00a0B. Remmel (Eds.). Birkh\u00e4user Boston, Boston, MA, 15\u201329."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129740"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00006-3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005114"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_2_1_9_1","unstructured":"Gianluca Curzi and Anupam Das. 2021. Cyclic Implicit Complexity. CoRR abs\/2110.01114(2021). arXiv:2110.01114https:\/\/arxiv.org\/abs\/2110.01114  Gianluca Curzi and Anupam Das. 2021. Cyclic Implicit Complexity. CoRR abs\/2110.01114(2021). arXiv:2110.01114https:\/\/arxiv.org\/abs\/2110.01114"},{"key":"e_1_3_2_1_10_1","unstructured":"Anupam Das. 2020. A circular version of G\u00f6del\u2019s T and its abstraction complexity. CoRR abs\/2012.14421(2020). arXiv:2012.14421https:\/\/arxiv.org\/abs\/2012.14421  Anupam Das. 2020. A circular version of G\u00f6del\u2019s T and its abstraction complexity. CoRR abs\/2012.14421(2020). arXiv:2012.14421https:\/\/arxiv.org\/abs\/2012.14421"},{"key":"e_1_3_2_1_11_1","volume-title":"On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci. 16, 1","author":"Das Anupam","year":"2020","unstructured":"Anupam Das . 2020. On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci. 16, 1 ( 2020 ). https:\/\/doi.org\/10.23638\/LMCS-16(1:1)2020 10.23638\/LMCS-16(1:1)2020 Anupam Das. 2020. On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci. 16, 1 (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:1)2020"},{"key":"e_1_3_2_1_12_1","volume-title":"6th International Conference on Formal Structures for Computation and Deduction, FSCD","author":"Das Anupam","year":"2021","unstructured":"Anupam Das . 2021. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs . In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 , July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)(LIPIcs, Vol.\u00a0195), Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 29:1\u201329:23. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.29 10.4230\/LIPIcs.FSCD.2021.29 Anupam Das. 2021. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)(LIPIcs, Vol.\u00a0195), Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 29:1\u201329:23. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.29"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"e_1_3_2_1_14_1","volume-title":"27th EACSL Annual Conference on Computer Science Logic (CSL 2018)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a0119)","author":"Das Anupam","year":"2018","unstructured":"Anupam Das and Damien Pous . 2018 . Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices) . In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a0119) , Dan Ghica and Achim Jung (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 19:1\u201319:18. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2018.19 10.4230\/LIPIcs.CSL.2018.19 Anupam Das and Damien Pous. 2018. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a0119), Dan Ghica and Achim Jung (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 19:1\u201319:18. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.19"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_2_1_17_1","volume-title":"TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings(Lecture Notes in Computer Science, Vol.\u00a011714)","author":"De Abhishek","year":"2019","unstructured":"Abhishek De and Alexis Saurin . 2019 . Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. In Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference , TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings(Lecture Notes in Computer Science, Vol.\u00a011714) , Serenella Cerrito and Andrei Popescu (Eds.). Springer, 297\u2013316. https:\/\/doi.org\/10.1007\/978-3-030-29026-9_17 10.1007\/978-3-030-29026-9_17 Abhishek De and Alexis Saurin. 2019. Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. In Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings(Lecture Notes in Computer Science, Vol.\u00a011714), Serenella Cerrito and Andrei Popescu (Eds.). Springer, 297\u2013316. https:\/\/doi.org\/10.1007\/978-3-030-29026-9_17"},{"key":"e_1_3_2_1_18_1","volume-title":"Computer Science Logic 2013 (CSL","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 Computer Science Logic 2013 (CSL 2013 ). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik . J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_19_1","volume-title":"11th International Workshop, CSL \u201997, Annual Conference of the EACSL","author":"Hofmann Martin","year":"1997","unstructured":"Martin Hofmann . 1997 . A Mixed Modal\/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion. In Computer Science Logic , 11th International Workshop, CSL \u201997, Annual Conference of the EACSL , Aarhus, Denmark , August 23-29, 1997, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a01414), Mogens Nielsen and Wolfgang Thomas (Eds.). Springer, 275\u2013294. https:\/\/doi.org\/10.1007\/BFb0028020 10.1007\/BFb0028020 Martin Hofmann. 1997. A Mixed Modal\/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion. In Computer Science Logic, 11th International Workshop, CSL \u201997, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a01414), Mogens Nielsen and Wolfgang Thomas (Eds.). Springer, 275\u2013294. https:\/\/doi.org\/10.1007\/BFb0028020"},{"key":"e_1_3_2_1_20_1","volume-title":"Introduction to Metamathematics(7 ed.)","author":"Kleene Stephen\u00a0Cole","unstructured":"Stephen\u00a0Cole Kleene . 1971. Introduction to Metamathematics(7 ed.) . Wolters-Noordhoff Publishing . Stephen\u00a0Cole Kleene. 1971. Introduction to Metamathematics(7 ed.). Wolters-Noordhoff Publishing."},{"key":"e_1_3_2_1_21_1","volume-title":"The logical strength of B\u00fcchi\u2019s decidability theorem. Log. Methods Comput. Sci. 15, 2","author":"Kolodziejczyk Leszek\u00a0Aleksander","year":"2019","unstructured":"Leszek\u00a0Aleksander Kolodziejczyk , Henryk Michalewski , Pierre Pradic , and Michal Skrzypczak . 2019. The logical strength of B\u00fcchi\u2019s decidability theorem. Log. Methods Comput. Sci. 15, 2 ( 2019 ). https:\/\/doi.org\/10.23638\/LMCS-15(2:16)2019 10.23638\/LMCS-15(2:16)2019 Leszek\u00a0Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. 2019. The logical strength of B\u00fcchi\u2019s decidability theorem. Log. Methods Comput. Sci. 15, 2 (2019). https:\/\/doi.org\/10.23638\/LMCS-15(2:16)2019"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434282"},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991)","author":"Leivant Daniel","year":"1991","unstructured":"Daniel Leivant . 1991 . A Foundational Delineation of Computational Feasiblity . In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991) , Amsterdam, The Netherlands , July 15-18, 1991. IEEE Computer Society, 2\u201311. https:\/\/doi.org\/10.1109\/LICS.1991.151625 10.1109\/LICS.1991.151625 Daniel Leivant. 1991. A Foundational Delineation of Computational Feasiblity. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), Amsterdam, The Netherlands, July 15-18, 1991. IEEE Computer Society, 2\u201311. https:\/\/doi.org\/10.1109\/LICS.1991.151625"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00040-2"},{"key":"e_1_3_2_1_25_1","volume-title":"8th International Workshop, CSL \u201994","author":"Leivant Daniel","year":"1994","unstructured":"Daniel Leivant and Jean-Yves Marion . 1994 . Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space. In Computer Science Logic , 8th International Workshop, CSL \u201994 , Kazimierz, Poland , September 25-30, 1994, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a0933), Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer, 486\u2013500. https:\/\/doi.org\/10.1007\/BFb0022277 10.1007\/BFb0022277 Daniel Leivant and Jean-Yves Marion. 1994. Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space. In Computer Science Logic, 8th International Workshop, CSL \u201994, Kazimierz, Poland, September 25-30, 1994, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a0933), Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer, 486\u2013500. https:\/\/doi.org\/10.1007\/BFb0022277"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01091743"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610056"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"e_1_3_2_1_31_1","unstructured":"Marc Wirz. 1999. Characterizing the Grzegorczyk hierarchy by safe recursion.  Marc Wirz. 1999. Characterizing the Grzegorczyk hierarchy by safe recursion."}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:09Z","timestamp":1750186929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":30,"alternative-id":["10.1145\/3531130.3533340","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533340","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}