{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:06:35Z","timestamp":1746245195842,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908965","type":"print"},{"value":"9783031908972","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a proof-theoretic analysis of the modal <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu \\textsf {LL}_{\\Box }^{\\infty }$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>\u03bc<\/mml:mi>\n                    <mml:msubsup>\n                      <mml:mi>LL<\/mml:mi>\n                      <mml:mrow>\n                        <mml:mo>\u25a1<\/mml:mo>\n                      <\/mml:mrow>\n                      <mml:mi>\u221e<\/mml:mi>\n                    <\/mml:msubsup>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, which is a linear version of the modal <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-calculus, intertwining the modalities from the modal <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu \\textsf {LL}_{\\Box }^{\\infty }$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>\u03bc<\/mml:mi>\n                    <mml:msubsup>\n                      <mml:mi>LL<\/mml:mi>\n                      <mml:mrow>\n                        <mml:mo>\u25a1<\/mml:mo>\n                      <\/mml:mrow>\n                      <mml:mi>\u221e<\/mml:mi>\n                    <\/mml:msubsup>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> and (ii) translating proofs of the modal mu-calculus into this new system via a \u201clinear translation\u201d, allowing us to extract the cut-elimination result.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_7","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:44:40Z","timestamp":1746189880000},"page":"133-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the cut-elimination of the modal $$\\mu $$-calculus: Linear Logic to the rescue"],"prefix":"10.1007","author":[{"given":"Esa\u00efe","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Afshari, B., Leigh, G.E.: Cut-free completeness for modal mu-calculus. In: 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201312 (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005088","DOI":"10.1109\/LICS.2017.8005088"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Log. 13(1), 2:1\u20132:44 (2012). https:\/\/doi.org\/10.1145\/2071368.2071370. URL https:\/\/doi.org\/10.1145\/2071368.2071370","DOI":"10.1145\/2071368.2071370"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Baelde, D., Doumane, A., Kuperberg, D., Saurin, A.: Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In: Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201922. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3531130.3533375. URL https:\/\/doi.org\/10.1145\/3531130.3533375","DOI":"10.1145\/3531130.3533375"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary Proof Theory: the Multiplicative Additive Case. In: CSL 2016, LIPIcs, vol.\u00a062, pp. 42:1\u201342:17 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.42. URL http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2016\/6582","DOI":"10.4230\/LIPIcs.CSL.2016.42"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bauer, E., Laurent, O.: Super exponentials in linear logic. Electronic Proceedings in Theoretical Computer Science 353, 50\u201373 (2021). https:\/\/doi.org\/10.4204\/eptcs.353.3. URL http:\/\/dx.doi.org\/10.4204\/EPTCS.353.3","DOI":"10.4204\/eptcs.353.3"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Br\u00fcnnler, K., Studer, T.: Syntactic cut-elimination for a fragment of the modal mu-calculus. Annals of Pure and Applied Logic 163(12), 1838\u20131853 (2012). https:\/\/doi.org\/10.1016\/j.apal.2012.04.006. URL https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0168007212000760","DOI":"10.1016\/j.apal.2012.04.006"},{"key":"7_CR7","unstructured":"Buss, S.R. (ed.): Handbook of Proof Theory. Elsevier, New York (1998)"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair reactive programming. In: S.\u00a0Jagannathan, P.\u00a0Sewell (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, pp. 361\u2013372. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535881. URL https:\/\/doi.org\/10.1145\/2535838.2535881","DOI":"10.1145\/2535838.2535881"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Curien, P., Herbelin, H.: The duality of computation. In: ICFP 2000, pp. 233\u2013243. ACM (2000). https:\/\/doi.org\/10.1145\/351240.351262. URL https:\/\/doi.org\/10.1145\/351240.351262","DOI":"10.1145\/351240.351262"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Danos, V., Joinet, J., Schellinx, H.: A new deconstructive logic: Linear logic. J. Symb. Log. 62(3), 755\u2013807 (1997). https:\/\/doi.org\/10.2307\/2275572. URL https:\/\/doi.org\/10.2307\/2275572","DOI":"10.2307\/2275572"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Derakhshan, F., Pfenning, F.: Circular proofs as session-typed processes: A local validity condition. Logical Methods in Computer Science Volume 18, Issue 2, 8 (2022). https:\/\/doi.org\/10.46298\/lmcs-18(2:8)2022. URL https:\/\/lmcs.episciences.org\/5675","DOI":"10.46298\/lmcs-18(2:8)2022"},{"key":"7_CR12","unstructured":"Doumane, A.: On the infinitary proof theory of logics with fixed points. Phd thesis, Paris Diderot University (2017)"},{"key":"7_CR13","unstructured":"Fukuda, Y., Yoshimizu, A.: A linear-logical reconstruction of intuitionistic modal logic S4. CoRR abs\/1904.10605 (2019). URL http:\/\/arxiv.org\/abs\/1904.10605"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4. URL https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Light linear logic 143(2), 175\u2013204 (1998). https:\/\/doi.org\/10.1006\/inco.1998.2700","DOI":"10.1006\/inco.1998.2700"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"J\u00e4ger, G., Kretz, M., Studer, T.: Canonical completeness of infinitary $$\\mu $$. The Journal of Logic and Algebraic Programming 76(2), 270\u2013292 (2008). https:\/\/doi.org\/10.1016\/j.jlap.2008.02.005. URL https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1567832608000209. Logic and Information: From Logic to Constructive Reasoning","DOI":"10.1016\/j.jlap.2008.02.005"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6. URL https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1\u20132), 163\u2013180 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2003.10.018","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Martini, S., Masini, A.: A modal view of linear logic. Journal of Symbolic Logic 59(3), 888\u2013899 (1994). https:\/\/doi.org\/10.2307\/2275915","DOI":"10.2307\/2275915"},{"key":"7_CR20","unstructured":"Miller, D.: Finding unity in computational logic. In: Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS \u201910. BCS Learning & Development Ltd., Swindon, GBR (2010)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Mints, G.: Effective cut-elimination for a fragment of modal mu-calculus. Studia Logica: An International Journal for Symbolic Logic 100(1\/2), 279\u2013287 (2012). URL http:\/\/www.jstor.org\/stable\/41475226","DOI":"10.1007\/s11225-012-9378-y"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Mints, G., Studer, T.: Cut-elimination for the mu-calculus with one variable. Electronic Proceedings in Theoretical Computer Science 77, 47\u201354 (2012). https:\/\/doi.org\/10.4204\/eptcs.77.7. URL http:\/\/dx.doi.org\/10.4204\/EPTCS.77.7","DOI":"10.4204\/eptcs.77.7"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: PPDP 2009, p. 129\u2013140. ACM, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1599410.1599427. URL https:\/\/doi.org\/10.1145\/1599410.1599427","DOI":"10.1145\/1599410.1599427"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: Games for the $$\\mu $$-calculus. Theoretical Computer Science 163(1), 99\u2013116 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00136-0. URL https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397595001360","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Pagani, M., Tortora\u00a0de Falco, L.: Strong normalization property for second order linear logic. Theoretical Computer Science 411(2), 410\u2013444 (2010)","DOI":"10.1016\/j.tcs.2009.07.053"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: M.\u00a0Nielsen, U.\u00a0Engberg (eds.) Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2303, pp. 357\u2013371. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_25. URL https:\/\/doi.org\/10.1007\/3-540-45931-6_25","DOI":"10.1007\/3-540-45931-6_25"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Santocanale, L.H.M.l., Fortier, J.: Cuts for circular proofs: semantics and cut-elimination. In: Computer Science Logic 2013, LIPIcs, vol.\u00a023, pp. 248\u2013262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Torino, Italy (2013). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.248. URL https:\/\/hal.science\/hal-01260986","DOI":"10.4230\/LIPIcs.CSL.2013.248"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Saurin, A.: A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points. TABLEAUX \u201923. Springer (2023). URL https:\/\/hal.science\/hal-04169137","DOI":"10.1007\/978-3-031-43513-3_12"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Schellinx, H.: A Linear Approach to Modal Proof Theory, pp. 33\u201343. Springer Netherlands, Dordrecht (1996). https:\/\/doi.org\/10.1007\/978-94-017-2798-3_3. URL https:\/\/doi.org\/10.1007\/978-94-017-2798-3_3","DOI":"10.1007\/978-94-017-2798-3_3"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Stirling, C.: Modal and Temporal Logics. In: Handbook of Logic in Computer Science. Oxford University Press (1992). https:\/\/doi.org\/10.1093\/oso\/9780198537618.003.0005. URL https:\/\/doi.org\/10.1093\/oso\/9780198537618.003.0005","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: M.\u00a0Maffei, E.\u00a0Tuosto (eds.) Trustworthy Global Computing, pp. 159\u2013175. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-662-45917-1_11"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:44:48Z","timestamp":1746189888000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}