Difference between revisions of "Matching Logic Explained"

From FSL
Jump to: navigation, search
 
Line 1: Line 1:
 +
== Technical Report ==
 +
<pubbib id='chen-lucanu-rosu-2020-trb' template='PubDefaultWithAbstractAndTitle'/>
 
<private>
 
<private>
 
== J'LAMP 2020 Submission ==
 
== J'LAMP 2020 Submission ==
 
<pubbib id='chen-lucanu-rosu-2020-jlamp-submission' template='PubDefaultWithAbstractAndTitle'/>
 
<pubbib id='chen-lucanu-rosu-2020-jlamp-submission' template='PubDefaultWithAbstractAndTitle'/>
 
</private>
 
</private>

Latest revision as of 02:52, 29 July 2020

[edit] Technical Report

Matching Logic Explained
Xiaohong Chen and Dorel Lucanu and Grigore Rosu
Technical Report http://hdl.handle.net/2142/107794, July 2020
Abstract. Matching logic was recently proposed as a unifying logic for specifying and reasoning about static structure and dynamic behavior of programs. In matching logic, patterns and specifications are used to uniformly represent mathematical domains (such as numbers and Boolean values), datatypes, and transition systems, whose properties can be reasoned about using one fixed matching logic proof system. In this paper we give a tutorial to matching logic. We use a suite of examples to explain the basic concepts of matching logic and show how to capture many important mathematical domains, datatypes, and transition systems using patterns and specifications. We put special emphasis on the general principles of induction and coinduction in matching logic and show how to do inductive and coinductive reasoning about datatypes and codatatypes. To encourage the development of the future tools for matching logic, we propose and use throughout the paper a human-readable formal syntax to write specifications in a modular and compact way.
PDF, Matching Logic, DOI, BIB


Personal tools
Namespaces

Variants
Actions
Navigation