TY - JOUR
T1 - Capturing constrained constructor patterns in matching logic
AU - Chen, Xiaohong
AU - Lucanu, Dorel
AU - Roşu, Grigore
N1 - The work presented in this paper was supported in part by NSF CNS 16-19275 . This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092 .
PY - 2023/1
Y1 - 2023/1
N2 - Reachability logic for rewrite theories consists of a specification of system states that are given by constrained constructor patterns, a transition relation that is given by a rewrite theory, and reachability properties expressed as pairs of state specifications. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It is known that reachability properties can be naturally expressed in matching logic. In this paper, we show that constrained constructor patterns can be faithfully specified as a matching logic theory. As a result, we obtain a full encoding of reachability logic for rewrite theories as matching logic theories, by combining the two encodings. We also show that the main properties of constrained constructor patterns can be specified and proved within matching logic, using the existing proof system.
AB - Reachability logic for rewrite theories consists of a specification of system states that are given by constrained constructor patterns, a transition relation that is given by a rewrite theory, and reachability properties expressed as pairs of state specifications. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It is known that reachability properties can be naturally expressed in matching logic. In this paper, we show that constrained constructor patterns can be faithfully specified as a matching logic theory. As a result, we obtain a full encoding of reachability logic for rewrite theories as matching logic theories, by combining the two encodings. We also show that the main properties of constrained constructor patterns can be specified and proved within matching logic, using the existing proof system.
KW - Constrained constructor patterns
KW - Matching logic
KW - Order-sorted algebras
UR - http://www.scopus.com/inward/record.url?scp=85138176043&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85138176043&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2022.100810
DO - 10.1016/j.jlamp.2022.100810
M3 - Article
AN - SCOPUS:85138176043
SN - 2352-2208
VL - 130
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
M1 - 100810
ER -