Initial Algebra Semantics in Matching Logic

Chen, Xiaohong; Lucanu, Dorel; Roşu, Grigore

Permalink

https://hdl.handle.net/2142/107781 Copy

Description

Title

Initial Algebra Semantics in Matching Logic

Author(s)

• Chen, Xiaohong
• Lucanu, Dorel
• Roşu, Grigore

Issue Date

2020-07

Keyword(s)

• Initial algebra semantics
• matching logic
• induction

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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/107781

Owning Collections