% Encoding: UTF-8
@TechReport{chen-lucanu-rosu-2020-tr,
author = {Xiaohong Chen and Dorel Lucanu and Grigore Ro\c{s}u},
institution = {University of Illinois at Urbana-Champaign},
title = {Initial algebra semantics in matching logic},
year = {2020},
month = jul,
number = {http://hdl.handle.net/2142/107781},
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.},
author_id = {Xiaohong Chen and Dorel Lucanu and Grigore Rosu},
category = {fsl,matching_logic,program_verification},
hidden = {false},
project_name = {Matching Logic},
project_url = {http://www.matching-logic.org},
}
@Comment{jabref-meta: databaseType:bibtex;}