Matching mu-Logic

From FSL
Revision as of 01:26, 26 November 2019 by Xiaohong (Talk | contribs)

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

LICS 2019

Matching mu-Logic
Xiaohong Chen and Grigore Rosu
LICS'19, ACM/IEEE. 2019. To appear
Abstract. Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching mu-logic, an extension of matching logic with a least fixpoint mu-binder. It is shown that matching mu-logic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal mu-logic as well as dynamic logic and various temporal logics such as infinite/finite-trace linear temporal logic and computation tree logic, and notably reachability logic, the underlying logic of the K framework for programming language semantics and formal analysis. Matching mu-logic therefore serves as a unifying foundation for specifying and reasoning about fixpoints and induction, programming languages and program specification and verification.
PDF, Slides(PPTX), Matching Logic, LICS'19, BIB

CALCO 2019

Matching mu-Logic: Foundation of K Framework
Xiaohong Chen and Grigore Rosu
CALCO'19, Leibniz International Proceedings in Informatics (LIPIcs) 139, pp 1-4. 2019
Abstract. K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.
PDF, Slides(PPTX), Matching Logic, DOI, CALCO'19, BIB

Technical Report

Matching mu-Logic
Xiaohong Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/102281, January 2019
Abstract. Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching mu-logic, an extension of matching logic with a least fixpoint mu-binder. It is shown that matching mu-logic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal mu-logic as well as dynamic logic and various temporal logics such as infinite/finite-trace linear temporal logic and computation tree logic, and notably reachability logic, the underlying logic of the K framework for programming language semantics and formal analysis. Matching mu-logic therefore serves as a unifying foundation for specifying and reasoning about fixpoints and induction, programming languages and program specification and verification.
PDF, Matching Logic, DOI, BIB


Personal tools
Namespaces

Variants
Actions
Navigation