{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:22:18Z","timestamp":1758979338011,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["MR\/S035540\/1"],"award-info":[{"award-number":["MR\/S035540\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662138","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A proof theory of right-linear (\u03c9-)grammars via cyclic proofs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0142-3676","authenticated-orcid":false,"given":"Anupam","family":"Das","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0402-0391","authenticated-orcid":false,"given":"Abhishek","family":"De","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":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1972","unstructured":"Alfred V. Aho and Jeffrey D. Ullman. 1972. The theory of parsing, translation, and compiling. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0048939"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl036"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_4"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(77)80004-4"},{"key":"e_1_3_2_1_7_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree automata techniques and applications. https:\/\/inria.hal.science\/hal-03367725"},{"volume-title":"Regular algebra and finite machines","author":"Conway John H.","key":"e_1_3_2_1_8_1","unstructured":"John H. Conway. 1971. Regular algebra and finite machines. Chapman and Hall, London, UK."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.10.002"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533340"},{"key":"e_1_3_2_1_11_1","unstructured":"Anupam Das and Abhishek De. 2024. A proof theory of right-linear (omega-)grammars via cyclic proofs. arXiv:2401.13382 [cs.LO]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.29007\/hzq3"},{"key":"e_1_3_2_1_13_1","unstructured":"Anupam Das and Damien Pous. 2017. A cut-free cyclic proof system for Kleene algebra. https:\/\/hal.science\/hal-01558132 Preprint. https:\/\/hal.science\/hal-01558132."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.10.008"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.126.4"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68954-8_5"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2022.23"},{"key":"e_1_3_2_1_20_1","volume-title":"Concurrent Kleene Algebra. In CONCUR 2009 - Concurrency Theory, Mario Bravetti and Gianluigi Zavattaro (Eds.). Springer Berlin Heidelberg","author":"Tony Hoare C. A. R.","year":"2009","unstructured":"C. A. R. Tony Hoare, Bernhard M\u00f6ller, Georg Struth, and Ian Wehrman. 2009. Concurrent Kleene Algebra. In CONCUR 2009 - Concurrency Theory, Mario Bravetti and Gianluigi Zavattaro (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 399--414."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(75)90009-5"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:STUD.0000032089.54776.63"},{"key":"e_1_3_2_1_23_1","volume-title":"Introduction to automata theory, languages, and computation","author":"Ullman Jeffrey D.","unstructured":"Jeffrey D. Ullman John E. Hopcroft, Rajeev Motwani. 2001. Introduction to automata theory, languages, and computation (2nd ed ed.). Addison-Wesley, USA.","edition":"2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-002"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"volume-title":"On action algebras","author":"Kozen Dexter","key":"e_1_3_2_1_27_1","unstructured":"Dexter Kozen. 1994. On action algebras. MIT Press, Cambridge, MA, USA, 78--88."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"volume-title":"Relational and Algebraic Methods in Computer Science, Wolfram Kahl and Timothy G","author":"Kozen Dexter","key":"e_1_3_2_1_30_1","unstructured":"Dexter Kozen and Alexandra Silva. 2012. Left-Handed Completeness. In Relational and Algebraic Methods in Computer Science, Wolfram Kahl and Timothy G. Griffin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 162--178."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.10.040"},{"volume-title":"Kleene algebra with tests: Completeness and decidability","author":"Kozen Dexter","key":"e_1_3_2_1_32_1","unstructured":"Dexter Kozen and Frederick Smith. 1997. Kleene algebra with tests: Completeness and decidability. In Computer Science Logic, Dirk van Dalen and Marc Bezem (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 244--259."},{"volume-title":"A complete system of B-rational identities","author":"Daniel KROB.","key":"e_1_3_2_1_33_1","unstructured":"Daniel KROB. 1990. A complete system of B-rational identities. In Automata, Languages and Programming, Michael S. Paterson (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 60--73."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2019.45"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.29"},{"volume-title":"Towards Kleene Algebra with recursion","author":"Lei\u00df Haas","key":"e_1_3_2_1_36_1","unstructured":"Haas Lei\u00df. 1992. Towards Kleene Algebra with recursion. In Computer Science Logic, Egon B\u00f6rger, Gerhard J\u00e4ger, Hans Kleine B\u00fcning, and Michael M. Richter (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 242--256."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.6"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(76)90415-0"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90023-0"},{"key":"e_1_3_2_1_40_1","volume-title":"Fixed-point characterization of context-free \u221e-languages. Information and control 61, 3","author":"Niwi\u0144ski Damian","year":"1984","unstructured":"Damian Niwi\u0144ski. 1984. Fixed-point characterization of context-free \u221e-languages. Information and control 61, 3 (1984), 247--276."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.26"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.05.004"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"volume-title":"The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Edward N","author":"Troquard Nicolas","key":"e_1_3_2_1_46_1","unstructured":"Nicolas Troquard and Philippe Balbiani. 2023. Propositional Dynamic Logic. In The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Edward N. Zalta and Uri Nodelman (Eds.). Metaphysics Research Lab, Stanford University, USA."},{"key":"e_1_3_2_1_47_1","first-page":"337","article-title":"Eine Axiomatisierung der Theorie der regul\u00e4ren Folgenmengen","volume":"12","author":"Wagner Klaus W.","year":"1976","unstructured":"Klaus W. Wagner. 1976. Eine Axiomatisierung der Theorie der regul\u00e4ren Folgenmengen. J. Inf. Process. Cybern. 12, 7 (1976), 337--354.","journal-title":"J. Inf. Process. Cybern."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.161.7"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"],"location":"Tallinn Estonia","acronym":"LICS '24"},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662138","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662138","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:06:21Z","timestamp":1750291581000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":48,"alternative-id":["10.1145\/3661814.3662138","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662138","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}