{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:05:54Z","timestamp":1760731554640,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"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"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21-CE48-019-01"],"award-info":[{"award-number":["ANR-21-CE48-019-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533375","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":14,"title":["Bouncing Threads for Circular and Non-Wellfounded Proofs"],"prefix":"10.1145","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[{"name":"IRISA, ENS Rennes, France"}]},{"given":"Amina","family":"Doumane","sequence":"additional","affiliation":[{"name":"LIP, CNRS and ENS de Lyon, France"}]},{"given":"Denis","family":"Kuperberg","sequence":"additional","affiliation":[{"name":"LIP, CNRS and ENS Lyon, France"}]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[{"name":"IRIF, CNRS, Universit\u00e9 Paris Cit\u00e9 and INRIA, France"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_19"},{"key":"e_1_3_2_1_2_1","volume-title":"Compositional Coinduction with Sized Types. (2016). Abstract for the invited talk at the 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS","author":"Abel Andreas","year":"2016","unstructured":"Andreas Abel . 2016. Compositional Coinduction with Sized Types. (2016). Abstract for the invited talk at the 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016 ), Eindhoven, the Netherlands , 2-3 April 2016. Andreas Abel. 2016. Compositional Coinduction with Sized Types. (2016). Abstract for the invited talk at the 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016), Eindhoven, the Netherlands, 2-3 April 2016."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_3_2_1_6_1","volume-title":"Bouncing Threads for Circular and Non-wellfounded Proofs (extended version). (June","author":"Baelde David","year":"2022","unstructured":"David Baelde , Amina Doumane , Denis Kuperberg , and Alexis Saurin . 2022. Bouncing Threads for Circular and Non-wellfounded Proofs (extended version). (June 2022 ). long version of the present paper, available at https:\/\/hal.archives-ouvertes.fr\/hal-03682126. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. 2022. Bouncing Threads for Circular and Non-wellfounded Proofs (extended version). (June 2022). long version of the present paper, available at https:\/\/hal.archives-ouvertes.fr\/hal-03682126."},{"key":"e_1_3_2_1_7_1","volume-title":"Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015","author":"Baelde David","year":"2015","unstructured":"David Baelde , Amina Doumane , and Alexis Saurin . 2015 . Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015 , September 7-10, 2015, Berlin, Germany(LIPIcs), Stephan Kreutzer (Ed.). Vol.\u00a041. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 549\u2013566. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2015.549 10.4230\/LIPIcs.CSL.2015.549 David Baelde, Amina Doumane, and Alexis Saurin. 2015. Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany(LIPIcs), Stephan Kreutzer (Ed.). Vol.\u00a041. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 549\u2013566. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2015.549"},{"key":"e_1_3_2_1_8_1","volume-title":"Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016","author":"Baelde David","year":"2016","unstructured":"David Baelde , Amina Doumane , and Alexis Saurin . 2016 . Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 , August 29 - September 1, 2016, Marseille, France(LIPIcs), Vol.\u00a062. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 42:1\u201342:17. http:\/\/www.dagstuhl.de\/dagpub\/978-3-95977-022-4 David Baelde, Amina Doumane, and Alexis Saurin. 2016. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France(LIPIcs), Vol.\u00a062. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 42:1\u201342:17. http:\/\/www.dagstuhl.de\/dagpub\/978-3-95977-022-4"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.176.0525"},{"volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","key":"e_1_3_2_1_10_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions . Springer . https:\/\/doi.org\/10.1007\/978-3-662-07964-5 10.1007\/978-3-662-07964-5 Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer. https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_11_1","volume-title":"SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings(Lecture Notes in Computer Science), Markus M\u00fcller-Olmand Helmut Seidl (Eds.). Vol.\u00a08723","author":"Brotherston James","year":"2014","unstructured":"James Brotherston and Nikos Gorogiannis . 2014 . Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In Static Analysis - 21st International Symposium , SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings(Lecture Notes in Computer Science), Markus M\u00fcller-Olmand Helmut Seidl (Eds.). Vol.\u00a08723 . Springer, 68\u201384. https:\/\/doi.org\/10.1007\/978-3-319-10936-7_5 10.1007\/978-3-319-10936-7_5 James Brotherston and Nikos Gorogiannis. 2014. Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings(Lecture Notes in Computer Science), Markus M\u00fcller-Olmand Helmut Seidl (Eds.). Vol.\u00a08723. Springer, 68\u201384. https:\/\/doi.org\/10.1007\/978-3-319-10936-7_5"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535881"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_2_1_15_1","first-page":"1","article-title":"Canonical proof-objects for coinductive programming: infinets with infinitely many cuts","volume":"7","author":"De Abhishek","year":"2021","unstructured":"Abhishek De , Luc Pellissier , and Alexis Saurin . 2021 . Canonical proof-objects for coinductive programming: infinets with infinitely many cuts . In PPDP. ACM , 7 : 1 \u2013 7 :15. Abhishek De, Luc Pellissier, and Alexis Saurin. 2021. Canonical proof-objects for coinductive programming: infinets with infinitely many cuts. In PPDP. ACM, 7:1\u20137:15.","journal-title":"PPDP. ACM"},{"volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods \u2013 TABLEAUX 2019(Lecture Notes in Computer Science), Serenella Cerrito and Andrei Popescu (Eds.). Vol.\u00a011714","author":"De Abhishek","key":"e_1_3_2_1_16_1","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 \u2013 TABLEAUX 2019(Lecture Notes in Computer Science), Serenella Cerrito and Andrei Popescu (Eds.). Vol.\u00a011714 . Springer , 297\u2013316. https:\/\/doi.org\/10.1007\/3-540-44904-3_18 10.1007\/3-540-44904-3_18 Abhishek De and Alexis Saurin. 2019. Infinets: the parallel syntax for non-wellfounded proof-theory. In Automated Reasoning with Analytic Tableaux and Related Methods \u2013 TABLEAUX 2019(Lecture Notes in Computer Science), Serenella Cerrito and Andrei Popescu (Eds.). Vol.\u00a011714. Springer, 297\u2013316. https:\/\/doi.org\/10.1007\/3-540-44904-3_18"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933598"},{"key":"e_1_3_2_1_19_1","volume-title":"CSL 2013","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) , CSL 2013 , September 2-5, 2013, Torino, Italy(LIPIcs), Simona Ronchi\u00a0Della Rocca (Ed.). Vol.\u00a023. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 248\u2013262. J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy(LIPIcs), Simona Ronchi\u00a0Della Rocca (Ed.). Vol.\u00a023. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 248\u2013262."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686159"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. 1989. Towards a Geometry of Interaction. In Categories in Computer Science and Logic(Contemporary Mathematics). AMS 69\u2013108.  Jean-Yves Girard. 1989. Towards a Geometry of Interaction. In Categories in Computer Science and Logic(Contemporary Mathematics). AMS 69\u2013108.","DOI":"10.1090\/conm\/092\/1003197"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094629"},{"key":"e_1_3_2_1_25_1","volume-title":"The Size-Change Termination Principle for Constructor Based Languages. Logical Methods in Computer Science 10, 1","author":"Hyvernat Pierre","year":"2014","unstructured":"Pierre Hyvernat . 2014. The Size-Change Termination Principle for Constructor Based Languages. Logical Methods in Computer Science 10, 1 ( 2014 ). https:\/\/doi.org\/10.2168\/LMCS-10(1:11)2014 10.2168\/LMCS-10(1:11)2014 Pierre Hyvernat. 2014. The Size-Change Termination Principle for Constructor Based Languages. Logical Methods in Computer Science 10, 1 (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:11)2014"},{"key":"e_1_3_2_1_26_1","volume-title":"20th International Symposium, MFCS\u201995, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings(Lecture Notes in Computer Science), Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.). Vol.\u00a0969","author":"Janin David","year":"1995","unstructured":"David Janin and Igor Walukiewicz . 1995 . Automata for the Modal mu-Calculus and related Results. In Mathematical Foundations of Computer Science 1995 , 20th International Symposium, MFCS\u201995, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings(Lecture Notes in Computer Science), Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.). Vol.\u00a0969 . Springer, 552\u2013562. https:\/\/doi.org\/10.1007\/3-540-60246-1_160 10.1007\/3-540-60246-1_160 David Janin and Igor Walukiewicz. 1995. Automata for the Modal mu-Calculus and related Results. In Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS\u201995, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings(Lecture Notes in Computer Science), Jir\u00ed Wiedermann and Petr H\u00e1jek (Eds.). Vol.\u00a0969. Springer, 552\u2013562. https:\/\/doi.org\/10.1007\/3-540-60246-1_160"},{"key":"e_1_3_2_1_27_1","volume-title":"6th International Conference","author":"Kaivola Roope","year":"1995","unstructured":"Roope Kaivola . 1995 . Axiomatising Linear Time Mu-calculus. In CONCUR \u201995: Concurrency Theory , 6th International Conference , Philadelphia, PA, USA , August 21-24, 1995, Proceedings. 423\u2013437. Roope Kaivola. 1995. Axiomatising Linear Time Mu-calculus. In CONCUR \u201995: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings. 423\u2013437."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science, Vol.\u00a01584.","volume-title":"Monotone Fixed-Point Types and Strong Normalization","author":"Matthes Ralph","unstructured":"Ralph Matthes . 1998. Monotone Fixed-Point Types and Strong Normalization . In CSL, Georg Gottlob, Etienne Grandjean, and Katrin Seyr (Eds.). Lecture Notes in Computer Science, Vol.\u00a01584. Berlin , 298\u2013312. Ralph Matthes. 1998. Monotone Fixed-Point Types and Strong Normalization. In CSL, Georg Gottlob, Etienne Grandjean, and Katrin Seyr (Eds.). Lecture Notes in Computer Science, Vol.\u00a01584. Berlin, 298\u2013312."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01091743"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.4"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2002010"},{"volume-title":"Foundations of Software Science and Computation Structures(Lecture Notes in Computer Science), Mogens Nielsen and Uffe Engberg (Eds.). Vol.\u00a02303","author":"Santocanale Luigi","key":"e_1_3_2_1_36_1","unstructured":"Luigi Santocanale . 2002. A Calculus of Circular Proofs and Its Categorical Semantics . In Foundations of Software Science and Computation Structures(Lecture Notes in Computer Science), Mogens Nielsen and Uffe Engberg (Eds.). Vol.\u00a02303 . Springer , 357\u2013371. Luigi Santocanale. 2002. A Calculus of Circular Proofs and Its Categorical Semantics. In Foundations of Software Science and Computation Structures(Lecture Notes in Computer Science), Mogens Nielsen and Uffe Engberg (Eds.). Vol.\u00a02303. Springer, 357\u2013371."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(01)00098-6"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90031-X"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.026"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287593"},{"volume-title":"Completeness of Kozen\u2019s Axiomatisation of the Propositional mu-Calculus","author":"Walukiewicz Igor","key":"e_1_3_2_1_41_1","unstructured":"Igor Walukiewicz . 1995. Completeness of Kozen\u2019s Axiomatisation of the Propositional mu-Calculus . In LICS. IEEE Computer Society , 14\u201324. Igor Walukiewicz. 1995. Completeness of Kozen\u2019s Axiomatisation of the Propositional mu-Calculus. In LICS. IEEE Computer Society, 14\u201324."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2836"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Haifa Israel","acronym":"LICS '22"},"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.3533375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:10Z","timestamp":1750186930000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533375"}},"subtitle":["Towards Compositionality with Circular Proofs"],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":41,"alternative-id":["10.1145\/3531130.3533375","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533375","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"}}]}}