# Difference between revisions of "Initial Algebra Semantics in Matching Logic"

From FSL

Line 3: | Line 3: | ||

<pubbib id='chen-lucanu-rosu-2021-popl-submission' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='chen-lucanu-rosu-2021-popl-submission' template='PubDefaultWithAbstractAndTitle'/> | ||

</private> | </private> | ||

+ | == Technical Report == | ||

+ | <pubbib id='chen-lucanu-rosu-2020-tr' template='PubDefaultWithAbstractAndTitle'/> |

## Latest revision as of 04:05, 17 July 2020

## [edit] Technical Report

**Initial algebra semantics in matching logic**- Xiaohong Chen and Dorel Lucanu and Grigore Rosu
http://hdl.handle.net/2142/107781, July 2020**Technical Report**

*Abstract.*Matching logic is a unifying foundational logic for defining formal programming language semantics, which adopts a minimalist design with few primitive constructs that are enough to express all properties within a variety of logical systems, including FOL, separation logic, (dependent) type systems, modal mu-logic, and more. In this paper, we consider initial algebra semantics and show how to capture it by matching logic specifications. Formally, given an algebraic specification E that defines a set of sorts (of data) and a set of operations whose behaviors are defined by a set of equational axioms, we define a corresponding matching logic specification, denoted INITIALALGEBRA(E), whose models are exactly the initial algebras of E. Thus, we reduce initial E-algebra semantics to the matching logic specifications INITIALALGEBRA(E), and reduce extrinsic initial E-algebra reasoning, which includes inductive reasoning, to generic, intrinsic matching logic reasoning.

- PDF, Matching Logic, DOI, BIB