Formal Systems Laboratory

Connecting Constrained Constructor Patterns and Matching Logic

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.