@inproceedings{83c30d28c7714b3aa53d683d2d6be7d0,
title = "Matching μ-Logic",
author = "Xiaohong Chen and Grigore Rosu",
note = "Funding Information: We made two main contributions in this paper. Firstly, we proposed a new sound and complete proof system H for matching logic (ML). Secondly, we extended ML with the least fixpoint µ-binder and proposed matching µ-logic (MmL). We showed the expressiveness of MmL by defining a variety of common logics about induction/fixpoints/verification in MmL. We hope that MmL may serve as a promising unifying foundation for specifying and reasoning about induction, fixpoints, as well as model checking and program verification. Acknowledgments: We thank the anonymous reviewers for their valuable comments on drafts of this paper. The work presented in this paper was supported in part by NSF CNS 16-19275. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092. Publisher Copyright: {\textcopyright} 2019 IEEE.; 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 ; Conference date: 24-06-2019 Through 27-06-2019",
year = "2019",
month = jun,
doi = "10.1109/LICS.2019.8785675",
language = "English",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019",
}