@techreport{rosu-2014-tr,
author = {Grigore Ro\c{s}u},
title = {Matching Logic: A Logic for Structural Reasoning},
abstract = {
Matching logic is a first-order logic (FOL) variant to reason about structure.
Its sentences, called patterns, are constructed using
variables, symbols, connectives and quantifiers,
but no difference is made between function and predicate symbols.
In models, a pattern evaluates into a power-set domain (the set of values
that match it), in contrast to FOL where functions, predicates and
connectives map into a domain.
Matching logic generalizes several logical frameworks important for program
analysis, such as: propositional logic, algebraic specification,
FOL with equality, and separation logic.
Patterns allow for specifying separation requirements at any level
in any program configuration, not only in the heaps or stores, without
any special logical constructs for that: the very nature of pattern
matching is that if two structures are matched as part of a pattern, then
they can only be spatially separated.
Like FOL, matching logic can also be translated into pure predicate logic
with equality, but it also admits its own sound and complete proof system.
},
institution = {University of Illinois},
month = {Jan},
year = {2014},
number = {http://hdl.handle.net/2142/47004},
author_id = {Grigore Rosu},
category = {fsl,matching_logic,K,logics,program_verification,semantics,executable_semantics},
project_url = {http://matching-logic.org},
project_name = {Matching Logic},
hidden = {false},
}