{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T23:11:10Z","timestamp":1784848270372,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0917140"],"award-info":[{"award-number":["CCF-0917140"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,1]]},"abstract":"<jats:p>\n            The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is a well-structured but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call\n            <jats:italic>\u03bc<\/jats:italic>\n            MALL, satisfies two fundamental proof theoretic properties: we establish weak normalization for it, and we design a focused proof system that we prove complete with respect to the initial system. That second result provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We show how these foundations can be applied to intuitionistic logic.\n          <\/jats:p>","DOI":"10.1145\/2071368.2071370","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Least and Greatest Fixed Points in Linear Logic"],"prefix":"10.1145","volume":"13","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[{"name":"University of Minnesota"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037173"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/322326.322339"},{"key":"e_1_2_1_5_1","unstructured":"Baelde D. 2008a. A linear approach to the proof-theory of least and greatest fixed points. Ph.D. thesis Ecole Polytechnique. Baelde D. 2008a. A linear approach to the proof-theory of least and greatest fixed points. Ph.D. thesis Ecole Polytechnique."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.113"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02716-1_8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Baelde D.\n     and \n      \n      \n      Miller D\n      \n  \n  . \n  2007\n  . Least and greatest fixed points in linear logic. In Proceedings of the International Conference on Logic for Programming and Automated Reasoning (LPAR). \n  N. Dershowitz and A. Voronkov Eds\n  . Lecture Notes in Computer Science vol. \n  4790 92--106. Baelde D. and Miller D. 2007. Least and greatest fixed points in linear logic. In Proceedings of the International Conference on Logic for Programming and Automated Reasoning (LPAR) . N. Dershowitz and A. Voronkov Eds. Lecture Notes in Computer Science vol. 4790 92--106.","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_24"},{"key":"e_1_2_1_11_1","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt H."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_8"},{"key":"e_1_2_1_13_1","first-page":"49","article-title":"R\u00e9cursivit\u00e9 graphique (l\u00e8re partie): Categorie des fonctions recursives primitives formelles","volume":"27","author":"Burroni A.","year":"1986","journal-title":"Cah. Topologie Geom. Differ. Categoriques"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_15"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9091-0"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Danos V. Joinet J.-B. and \n      \n      \n      Schellinx H\n      \n  \n  . \n  1993\n  . The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Proceedings of the Kurt G\u00f6del Colloquium. G. Gottlob A. Leitsch and D. Mundici Eds. Lecture Notes in Computer Science vol. \n  713 Springer 159--171. Danos V. Joinet J.-B. and Schellinx H. 1993. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Proceedings of the Kurt G\u00f6del Colloquium . G. Gottlob A. Leitsch and D. Mundici Eds. Lecture Notes in Computer Science vol. 713 Springer 159--171.","DOI":"10.1007\/BFb0022564"},{"key":"e_1_2_1_18_1","volume-title":"London Mathematical Society Lecture Note Series","volume":"222","author":"Danos V."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.35"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.017"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_22_1","unstructured":"Girard J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu. Girard J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_2_1_26_1","unstructured":"Laurent O. 2002. Etude de la polarisation en logique. Ph.D. thesis Universit\u00e9 Aix-Marseille II. Laurent O. 2002. Etude de la polarisation en logique. Ph.D. thesis Universit\u00e9 Aix-Marseille II."},{"key":"e_1_2_1_27_1","unstructured":"Laurent O. 2004. A proof of the focalization property of linear logic. Unpublished note. Laurent O. 2004. A proof of the focalization property of linear logic. Unpublished note."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.11.002"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Liang C.\n     and \n      \n      \n      Miller D\n      \n  \n  . \n  2007\n  . Focusing and polarization in intuitionistic logic. In Proceedings of the International Workshop on Computer Science Logic. J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. \n  4646 Springer 451--465. Liang C. and Miller D. 2007. Focusing and polarization in intuitionistic logic. In Proceedings of the International Workshop on Computer Science Logic . J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. 4646 Springer 451--465.","DOI":"10.1007\/978-3-540-74915-8_34"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647848.736914"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00045-X"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Miller D.\n     and \n      \n      \n      Nigam V\n      \n  \n  . \n  2007\n  . Incorporating tables into proofs. In Proceedings of the International Workshop on Computer Science Logic. J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. \n  4646 Springer 466--480. Miller D. and Nigam V. 2007. Incorporating tables into proofs. In Proceedings of the International Workshop on Computer Science Logic . J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. 4646 Springer 466--480.","DOI":"10.1007\/978-3-540-74915-8_35"},{"key":"e_1_2_1_36_1","unstructured":"Miller D. and Pimentel E. 2010. A formal framework for specifying sequent calculus proof systems. Available from authors\u2019 Web sites. Miller D. and Pimentel E. 2010. A formal framework for specifying sequent calculus proof systems. Available from authors\u2019 Web sites."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.072"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Miller D.\n     and \n      \n      \n      Saurin A\n      \n  \n  . \n  2007\n  . From proofs to focused proofs: A modular proof of focalization in linear logic. In Proceedings of the International Workshop on Computer Science Logic. J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. \n  4646 Springer 405--419. Miller D. and Saurin A. 2007. From proofs to focused proofs: A modular proof of focalization in linear logic. In Proceedings of the International Workshop on Computer Science Logic . J. Duparc and T. A. Henzinger Eds. Lecture Notes in Computer Science vol. 4646 Springer 405--419.","DOI":"10.1007\/978-3-540-74915-8_31"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Momigliano A.\n     and \n      \n      \n      Tiu A\n      \n  \n  . \n  2003\n  . Induction and co-induction in sequent calculus. In Proceedings of the International Workshop on Types for Proofs and Programs. M. Coppo S. Berardi and F. Damiani Eds\n  . Lecture Notes in Computer Science vol. \n  3085 293--308. Momigliano A. and Tiu A. 2003. Induction and co-induction in sequent calculus. In Proceedings of the International Workshop on Types for Proofs and Programs . M. Coppo S. Berardi and F. Damiani Eds. Lecture Notes in Computer Science vol. 3085 293--308.","DOI":"10.1007\/978-3-540-24849-1_19"},{"key":"e_1_2_1_42_1","unstructured":"Nigam V. 2009. Exploiting non-canonicity in the sequent calculus. Ph.D. thesis Ecole Polytechnique. Nigam V. 2009. Exploiting non-canonicity in the sequent calculus. Ph.D. thesis Ecole Polytechnique."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Santocanale L. 2001. A calculus of circular proofs and its categorical semantics. BRICS Report Series RS-01-15 BRICS Department of Computer Science University of Aarhus. Santocanale L. 2001. A calculus of circular proofs and its categorical semantics. BRICS Report Series RS-01-15 BRICS Department of Computer Science University of Aarhus.","DOI":"10.7146\/brics.v8i15.20472"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287585"},{"key":"e_1_2_1_45_1","unstructured":"Tiu A. 2004. A logical framework for reasoning about logical specifications. Ph.D. thesis Pennsylvania State University. Tiu A. 2004. A logical framework for reasoning about logical specifications. Ph.D. thesis Pennsylvania State University."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_7"},{"key":"e_1_2_1_47_1","unstructured":"Tiu A. and Momigliano A. 2010. Cut elimination for a logic with induction and co-induction. CoRR abs\/1009.6171. Tiu A. and Momigliano A. 2010. Cut elimination for a logic with induction and co-induction. CoRR abs\/1009.6171."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Workshop on Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL\u201905)","author":"Tiu A."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071370","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071368.2071370","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:22Z","timestamp":1750241182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071368.2071370"],"URL":"https:\/\/doi.org\/10.1145\/2071368.2071370","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2009-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}