Connecting Constrained Constructor Patterns and Matching Logic

From FSL
Revision as of 20:11, 22 March 2020 by Xiaohong (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

WRLA 2020

Connecting Constrained Constructor Patterns and Matching Logic
Xiaohong Chen and Dorel Lucanu and Grigore Rosu
WRLA'20. 2020. To appear
Abstract. Constrained constructor patterns are built from pairs of constructor term patterns and a constraint expressed by a quantifier-free first order logic formula, using the conjunction and disjunction connector. They are used to express state predicates for reachability logic defined over rewrite theories. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It has been shown to capture several logics important for programming languages, including First-order logic with Fixpoints and order-sorted algebra. In this paper we investigate the relationship between the language of the constrained constructor patterns and matching logic. The results we obtained from this comparison bring a mutual benefit for the two approaches. The matching logic can borrow computationally effcient proofs for some equivalences, and the language of the constrained constructor patterns can get a more logical avor and more expressivity.
PDF, Matching Logic, WRLA'20, BIB

Personal tools
Namespaces

Variants
Actions
Navigation