@techreport{chen-rosu-2019-tr,
author = {Xiaohong Chen and Grigore Ro\c{s}u},
title = {Matching mu-Logic},
author_id = {Xiaohong Chen and Grigore Rosu},
category = {fsl,matching_logic,program_verification},
project_url = {http://www.matching-logic.org},
project_name = {Matching Logic},
institution = {University of Illinois at Urbana-Champaign},
month = {January},
year = {2019},
number = {http://hdl.handle.net/2142/102281},
abstract = {
Matching logic is a logic for specifying and reasoning about
structure by means of patterns and pattern matching.
This paper makes two contributions.
First, it proposes a sound and complete proof system for
matching logic in its full generality.
Previously, sound and complete deduction for matching logic
was known only for particular theories providing equality
and membership.
Second, it proposes matching mu-logic, an extension of
matching logic with a least fixpoint mu-binder.
It is shown that matching mu-logic captures as special instances many
important logics in mathematics and computer science, including
first-order logic with least fixpoints, modal mu-logic
as well as dynamic logic and various temporal logics such as
infinite/finite-trace linear temporal logic and computation tree logic,
and notably reachability logic, the underlying logic of the K framework
for programming language semantics and formal analysis.
Matching mu-logic therefore serves as a unifying foundation for
specifying and reasoning about fixpoints and induction,
programming languages and program specification and verification.
},
hidden = {false},
}