Connecting Constrained Constructor Patterns and Matching Logic

Xiaohong Chen, Dorel Lucanu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Constrained constructor patterns are pairs of a constructor term pattern and a quantifier-free first-order logic constraint, built from conjunction and disjunction. 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 logical systems and/or models that are important for programming languages, including first-order logic with fixpoints and order-sorted algebra. In this paper, we investigate the relationship between constrained constructor patterns and matching logic. The comparison result brings us a mutual benefit for the two approaches. Matching logic can borrow computationally efficient proofs for some equivalences, and the language of the constrained constructor patterns can get a more logical flavor and more expressiveness.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
EditorsSantiago Escobar, Narciso Martí-Oliet
Number of pages19
ISBN (Print)9783030635947
StatePublished - 2020
Event13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 - Virtual, Online
Duration: Oct 20 2020Oct 22 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12328 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Connecting Constrained Constructor Patterns and Matching Logic'. Together they form a unique fingerprint.

Cite this