TY - GEN

T1 - Matching logic

T2 - 13th International Conference on Algebraic Methodology and Software Technology, AMAST 2010

AU - Roşu, Grigore

AU - Ellison, Chucky

AU - Schulte, Wolfram

N1 - Funding Information:
Supported in part by NSF grants CCF-0916893, CNS-0720512, and CCF-0448501, by NASA contract NNL08AA23C, by a Samsung SAIT grant, and by several Microsoft gifts.

PY - 2011

Y1 - 2011

N2 - This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP's Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.

AB - This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP's Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.

UR - http://www.scopus.com/inward/record.url?scp=79551505824&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79551505824&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-17796-5_9

DO - 10.1007/978-3-642-17796-5_9

M3 - Conference contribution

AN - SCOPUS:79551505824

SN - 3642177956

SN - 9783642177958

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 142

EP - 162

BT - Algebraic Methodology and Software Technology - 13th International Conference, AMAST 2010, Revised Selected Papers

Y2 - 23 June 2010 through 25 June 2010

ER -