{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,28]],"date-time":"2025-12-28T02:21:13Z","timestamp":1766888473388,"version":"3.28.0"},"reference-count":39,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T00:00:00Z","timestamp":1687737600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T00:00:00Z","timestamp":1687737600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,6,26]]},"DOI":"10.1109\/lics56636.2023.10175772","type":"proceedings-article","created":{"date-parts":[[2023,7,14]],"date-time":"2023-07-14T17:18:23Z","timestamp":1689355103000},"page":"1-13","source":"Crossref","is-referenced-by-count":5,"title":["Computational expressivity of (circular) proofs with fixed points"],"prefix":"10.1109","author":[{"given":"Gianluca","family":"Curzi","sequence":"first","affiliation":[{"name":"University of Birmingham,Birmingham,UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anupam","family":"Das","sequence":"additional","affiliation":[{"name":"University of Birmingham,Birmingham,UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref13","first-page":"29:1","article-title":"On the logical strength of confluence and normalisation for cyclic proofs","volume":"195","author":"das","year":"2021","journal-title":"FSCD ’21"},{"key":"ref35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59971-2","article-title":"Subsystems of second order arithmetic","author":"simpson","year":"1999","journal-title":"Perspectives in Mathematical Logic"},{"key":"ref12","article-title":"On the logical complexity of cyclic arithmetic","volume":"16","author":"das","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479402"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"ref14","first-page":"35:1","article-title":"Phase semantics for linear logic with least and greatest fixed points","volume":"250","author":"de","year":"2022","journal-title":"FSTTCS ’22"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-008-9133-6"},{"key":"ref31","article-title":"Proof Theory","author":"rathjen","year":"2022","journal-title":"The Stanford Encyclopedia of Philosophy"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.2307\/421132"},{"key":"ref11","article-title":"A circular version of Gödel’s T and its abstraction complexity","author":"das","year":"2020","journal-title":"CoRR"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-017-0526-y"},{"journal-title":"Computational expressivity of (circular) proofs with fixed points","year":"2023","author":"curzi","key":"ref10"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"ref17","article-title":"On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes)","author":"doumane","year":"2017","journal-title":"PhD thesis"},{"article-title":"Lectures on the modal ?-calculus","year":"2008","author":"venema","key":"ref39"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_17"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1096901767"},{"key":"ref19","article-title":"On relation between totality semantic and syntactic validity","author":"ehrhard","year":"2021","journal-title":"TLLA ’21"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470664"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.2307\/2275338"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3434282"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"ref25","article-title":"Recursive types and type constraints in second-order lambda calculus","author":"paul mendler","year":"1987","journal-title":"Logic in Computer Science"},{"key":"ref20","article-title":"Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur","author":"girard","year":"1972","journal-title":"PhD thesis"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"ref27","article-title":"Generalized inductive definitions. The ?-calculus and $\\Pi _2^1$-comprehension","author":"m\u00f6llerfeld","year":"2002","journal-title":"PhD thesis"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201600096"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_3"},{"key":"ref7","first-page":"51","author":"brotherston","year":"2007","journal-title":"Complete sequent calculi for induction and infinite descent"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2012028"},{"key":"ref4","first-page":"42:1","article-title":"Infinitary proof theory: the multiplicative additive case","volume":"62","author":"baelde","year":"2016","journal-title":"CSL ’16"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533375"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2020.102903"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_9"}],"event":{"name":"2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2023,6,26]]},"location":"Boston, MA, USA","end":{"date-parts":[[2023,6,29]]}},"container-title":["2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10175635\/10175671\/10175772.pdf?arnumber=10175772","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,1]],"date-time":"2023-08-01T17:58:58Z","timestamp":1690912738000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10175772\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,26]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/lics56636.2023.10175772","relation":{},"subject":[],"published":{"date-parts":[[2023,6,26]]}}}