Difference between revisions of "Initial algebra semantics in matching logic"

From FSL
Jump to: navigation, search
(Created page with "== Technical Report == <pubbib id='chen-lucanu-rosu-2020-tr' template='PubDefaultWithAbstractAndTitle'/>")

Latest revision as of 19:36, 13 October 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