Files in this item



application/pdfMatching-Logic- ... r-Structural-Reasoning.pdf (232kB)


Title:Matching Logic: A Logic for Structural Reasoning
Author(s):Rosu, Grigore
Subject(s):first-order logic, separation logic, matching logic
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 dif ference 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.
Issue Date:2014-01-20
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2014-01-21

This item appears in the following Collection(s)

Item Statistics