From 9c74fe4b4cad651a9376cba498bf99290488ed91 Mon Sep 17 00:00:00 2001 From: Xiaohong Chen Date: Wed, 4 Jan 2023 15:17:48 -0600 Subject: [PATCH] Update index.md Revised the summary of the LICS'19 paper. --- index.md | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/index.md b/index.md index 85729c4..c5562a7 100644 --- a/index.md +++ b/index.md @@ -111,17 +111,29 @@ logic with the classic Hoare-style program verification. LMCS, 2017. - This paper is a comprehensive in-depth survey paper of the mathematical foundations of matching logic. The paper discusses the motivation of - matching logic and its usage in K, defines its syntax and semantics, + matching logic and its usage in the [K framework](https://kframework.org), + defines its syntax and semantics, shows that many logics can be defined as theories, including FOL, modal logic S5, and separation logic, and proposes a sound and - complete proof system. + complete proof system for theories that feature equality. - **Xiaohong Chen, Grigore Rosu**. *[Matching mu-Logic](https://fsl.cs.illinois.edu/publications/chen-rosu-2019-lics.html)*, LICS, 2019. - This paper is the canonical paper that proposes matching logic in its full - generality. It discuss more logics that can be defined in matching logic, including FOL - with least fixpoints, modal μ-logic, temporal logics, dynamic logic, - separation logic with recursive definitions, and reachability logic. + generality. It adds fixpoints to matching logic, as suggested by its name: + matching mu-logic, where "mu" is the operation that builds least fixpoints, as in + [modal mu-calculus](https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus). + To keep the name simple and consistent, we drop the "mu" and simply call it "matching logic" + in our current and future papers. + This paper discusses more logics that can be defined in matching logic, + including FOL with least fixpoints, modal μ-logic, temporal logics, dynamic logic, + separation logic with recursive definitions, and reachability logic (i.e., program verification). + One of the main contributions of the paper is the proposal of a new proof system for matching logic + that supports formal reasoning in all theories, and thus addressing + the limitation of the previous LMCS'17 proof system that it only works for equality-featuring theories. + The new proof system now serves as the foundation for formal reasoning in the K framework + and is used as a basis for generating machine-checkable correctness certificates for all K tools. + ### Other publications