{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:36:45Z","timestamp":1770295005019,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Natural Science Foundation","award":["NSF CNS 16-19275"],"award-info":[{"award-number":["NSF CNS 16-19275"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["No. FA8750-18-C-0092"],"award-info":[{"award-number":["No. FA8750-18-C-0092"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.<\/jats:p>","DOI":"10.1145\/3428229","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Towards a unified proof framework for automated fixpoint reasoning using matching logic"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3208-4061","authenticated-orcid":false,"given":"Xiaohong","family":"Chen","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Minh-Thai","family":"Trinh","sequence":"additional","affiliation":[{"name":"Advanced Digital Sciences Center, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nishant","family":"Rodrigues","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_24"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_13"},{"key":"e_1_2_2_6_1","volume-title":"Modal logic","author":"Blackburn Patrick","unstructured":"Patrick Blackburn , Maarten de Rijke , and Yde Venema . 2001. Modal logic . Cambridge University Press , New York, NY, USA . Patrick Blackburn, Maarten de Rijke, and Yde Venema. 2001. Modal logic. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.44.10.1061"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_13"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032278"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_2_2_12_1","volume-title":"Petersen","author":"Brotherston James","year":"2012","unstructured":"James Brotherston , Nikos Gorogiannis , and Rasmus L . Petersen . 2012 . A generic cyclic theorem prover. In Programming Languages and Systems, Ranjit Jhala and Atsushi Igarashi (Eds.). Springer , Kyoto, Japan, 350-367. James Brotherston, Nikos Gorogiannis, and Rasmus L. Petersen. 2012. A generic cyclic theorem prover. In Programming Languages and Systems, Ranjit Jhala and Atsushi Igarashi (Eds.). Springer, Kyoto, Japan, 350-367."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542667"},{"key":"e_1_2_2_15_1","first-page":"1","volume-title":"Matching-logic. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS'19)","author":"Chen Xiaohong","year":"2019","unstructured":"Xiaohong Chen and Grigore Ro\u015fu . 2019 . Matching-logic. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS'19) . ACM, Vancouver, Canada , 1 - 13 . Xiaohong Chen and Grigore Ro\u015fu. 2019. Matching-logic. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS'19). ACM, Vancouver, Canada, 1-13."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408970"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737984"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0289-4"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00240-X"},{"key":"e_1_2_2_25_1","volume-title":"Logics of Time and Computation (2. ed.). Number 7 in CSLI Lecture Notes","author":"Goldblatt Robert","unstructured":"Robert Goldblatt . 1992. Logics of Time and Computation (2. ed.). Number 7 in CSLI Lecture Notes . Center for the Study of Language and Information, Stanford, CA. Robert Goldblatt. 1992. Logics of Time and Computation (2. ed.). Number 7 in CSLI Lecture Notes. Center for the Study of Language and Information, Stanford, CA."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.27"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737979"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2"},{"key":"e_1_2_2_33_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1\u0161 Vojnar and Lijun Zhang (Eds.)","author":"Katelaan Jens","unstructured":"Jens Katelaan , Christoph Matheja , and Florian Zuleger . 2019. Efective Entailment Checking for Separation Logic with Inductive Definitions . In Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1\u0161 Vojnar and Lijun Zhang (Eds.) . Springer International Publishing , Cham , 319-336. Jens Katelaan, Christoph Matheja, and Florian Zuleger. 2019. Efective Entailment Checking for Separation Logic with Inductive Definitions. In Tools and Algorithms for the Construction and Analysis of Systems, Tom\u00e1\u0161 Vojnar and Lijun Zhang (Eds.). Springer International Publishing, Cham, 319-336."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009887"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012782"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_25"},{"key":"e_1_2_2_41_1","unstructured":"The Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project.  The Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_8"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75596-8_18"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/sefm.2006.7"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2002.1029817"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.23638\/lmcs13(4:28)2017"},{"key":"e_1_2_2_51_1","volume-title":"Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, and Zhilin Wu.","author":"Sighireanu Mihaela","year":"2019","unstructured":"Mihaela Sighireanu , Juan A. Navarro P\u00e9rez , Andrey Rybalchenko , Nikos Gorogiannis , Radu Iosif , Andrew Reynolds , Cristina Serban , Jens Katelaan , Christoph Matheja , Thomas Noll , Florian Zuleger , Wei-Ngan Chin , Quang Loc Le , Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, and Zhilin Wu. 2019 . SL-COMP: Competition of solvers for separation logic. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Stefen (Eds.). Springer International Publishing , Cham, 116-132. Mihaela Sighireanu, Juan A. Navarro P\u00e9rez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, and Zhilin Wu. 2019. SL-COMP: Competition of solvers for separation logic. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Stefen (Eds.). Springer International Publishing, Cham, 116-132."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0471-5"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_54_1","unstructured":"The Isabelle development team. 2018. Isabelle. https:\/\/isabelle.in.tum.de\/.  The Isabelle development team. 2018. Isabelle. https:\/\/isabelle.in.tum.de\/."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_30"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428229","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428229","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428229"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":53,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428229"],"URL":"https:\/\/doi.org\/10.1145\/3428229","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}