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

From FSL
Jump to: navigation, search
Line 3: Line 3:
<pubbib id='chen-lucanu-rosu-2021-popl-submission' template='PubDefaultWithAbstractAndTitle'/>
<pubbib id='chen-lucanu-rosu-2021-popl-submission' template='PubDefaultWithAbstractAndTitle'/>
== 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
Technical Report http://hdl.handle.net/2142/107781, July 2020
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

Personal tools