@article{rosu-2017-lmcs,
author = {Grigore Ro\c{s}u},
title = {Matching logic},
abstract = {
This paper presents ''matching logic'', a first-order logic (FOL)
variant for specifying and reasoning about structure by means of patterns and
pattern matching.
Its sentences, the ''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 and predicates
map into a regular domain.
Matching logic uniformly generalizes several logical frameworks important
for program analysis, such as: propositional logic, algebraic specification,
FOL with equality, modal logic, and separation logic.
Patterns can specify 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,
at the same time admitting its own sound and complete proof system.
A practical aspect of matching logic is that FOL reasoning with equality remains sound,
so off-the-shelf provers and SMT solvers can be used for matching logic
reasoning.
Matching logic is particularly well-suited for reasoning about programs
in programming languages that have an operational semantics, but
it is not limited to this.
},
journal = {Logical Methods in Computer Science},
year = {2017},
volume = {13},
number = {4},
pages = {1-61},
month = {December},
doi = {http://arxiv.org/abs/1705.06312},
author_id = {Grigore Rosu},
category = {fsl, executable_semantics, matching_logic, logics, K},
journal_acronym = {LMCS},
journal_url = {https://lmcs.episciences.org/4153},
project_acronym = {Matching Logic},
project_url = {http://www.matching-logic.org/index.php/Matching_Logic},
}