<p>I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti.</p>
<p>More precisely, my work focuses on:</p>
<ul>
<li>The translation from K into Dedukti that you mention (probably because you found this paper: <a href="https://doi.org/10.4230/LIPIcs.TYPES.2022.12" rel="nofollow noreferrer">https://doi.org/10.4230/LIPIcs.TYPES.2022.12</a>) is based on the translation from K into Matching Logic. Your translation interprets the Matching Logic operators to be able to execute programs into Dedukti.</li>
<li>A shallow encoding from Matching mu-Logic is available here: <a href="https://gitlab.com/semantiko/ML2DK" rel="nofollow noreferrer">https://gitlab.com/semantiko/ML2DK</a> (need to be updated). This encoding is a first step to recheck KProver proofs into Dedukti.</li>
</ul>
<p>The encodings of Applicative Matching Logic (AML) into Lean and Coq are deep and they want to formalize theoretical results about AML.</p>
<p>Could you tell us why you are interested in mechanizing Matching Logic?
The various projects carried out to formalize Matching Logic are not of the same nature, and do not involve the same version of Matching Logic.</p>

CC BY-SA 4.0
2023-09-08T16:15:26.853Z
I am interested for several reasons. 1. To understand matching logic better (cuz it is not very clear, which statements on that are proved, and how it compares to more well known logics) 2. To understand how (parametrized?) soundess/completeness usually look.
uhbif19
CC BY-SA 4.0
2023-09-08T16:16:42.697Z
Your work direction is very interesting BTW, I was heard of it before.
uhbif19
CC BY-SA 4.0
2023-08-16T20:45:35.333Z
2023-08-16T20:45:35.333Z
Amélie Ledein
<p>Okay, I need to admit that I am not best at googling. It already exists. Seems like the soundness is covered, and completeness only covered for non-mu part.</p>
<p><a href="https://arxiv.org/abs/2201.05716" rel="nofollow noreferrer">https://arxiv.org/abs/2201.05716</a></p>
<p>As for applicative version of matching logic, I did not find anything.</p>

CC BY-SA 4.0
2023-07-16T19:09:05.530Z
2023-07-16T19:09:05.530Z
uhbif19
<p>There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of any formalization covering completeness of matching logic (although there is a pen-and-paper proof in <a href="https://doi.org/10.1109/LICS.2019.8785675" rel="noreferrer">Matching μ-Logic</a>, and a <a href="https://is.muni.cz/th/mcbtk/thesis.pdf" rel="noreferrer">master's thesis</a>).</p>
<h1><a href="https://github.com/harp-project/AML-Formalization" rel="noreferrer">Applicative Matching Logic in Coq</a></h1>
<p>This formalization is still under development; <a href="https://doi.org/10.4204/EPTCS.369.2" rel="noreferrer">here is a paper about an earlier (middle of 2022) version of it</a>.
The current version covers:</p>
<ul>
<li>Syntax (using the locally nameless encoding of binders) including mu; semantics; proof system.</li>
<li>Soundness of the proof system.</li>
<li>A &quot;proof mode&quot; on top of the proof system - a set of tactics for constructing matching logic proofs interactively.</li>
<li>Theory of definedness/equality (both from a model-theoretical and proof-theoretical perspective).</li>
<li>Theory of sorts and natural numbers.</li>
<li>Many proof system theorems from <a href="https://doi.org/10.1109/LICS.2019.8785675" rel="noreferrer">Matching μ-Logic</a>, adapted to AML.</li>
<li>Deduction theorem - a proof (of the most general variant available in a <a href="http://hdl.handle.net/2142/102281" rel="noreferrer">technical report</a> accompanying the above-linked Matching μ-Logic paper), as well as an infrastructure for using that theorem.</li>
<li>Some other model theory (isomorphisms, &quot;model extension&quot;).</li>
</ul>
<h1><a href="https://gitlab.com/ilds/aml-lean/MatchingLogic" rel="noreferrer">Applicative Matching Logic in Lean</a></h1>
<ul>
<li>Syntax (using named encoding of binders) including mu; semantics; proof system.</li>
<li>Soundness of the proof system.</li>
<li><a href="https://gitlab.com/ilds/aml-lean/AML-Lean-to-Metamath" rel="noreferrer">Proof extraction into Metamath</a> (see the Metamath-based formalization below).</li>
<li>Deduction theorem for closed patterns.</li>
</ul>
<h1><a href="https://github.com/runtimeverification/proof-generation/blob/main/theory/matching-logic.mm" rel="noreferrer">Applicative Matching Logic in Metamath</a></h1>
<p>Introduced for <a href="https://doi.org/10.1007/978-3-030-81688-9_23" rel="noreferrer">proof object generation for the K Framework</a>.</p>
<ul>
<li>Syntax (using named encoding of binders) including mu.</li>
<li>Proof system.</li>
<li>Lots of lemmas using the proof system.</li>
</ul>
<h1><a href="https://gitlab.com/semantiko/kamelo" rel="noreferrer">A Translator from K into Dedukti</a></h1>

CC BY-SA 4.0
2023-08-16T14:07:22.023Z
Note that the Metamath proof generation includes a translation from K's kore to Matching Logic. Unfortunately it is not too well documented. 

https://github.com/runtimeverification/proof-generation/tree/main/src/proof_generation/kore
nishantjr
CC BY-SA 4.0
2023-08-15T09:32:07.767Z
2023-08-15T09:32:07.767Z
Jan Tušil
<p>Is there any mechanization for matching logic (any flavor)?</p>
<p>I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the framework.</p>

<fl.formal-languages><coq><formal-methods><operational-semantics><agda>
Formalization of matching logic (logic behind K Framework)
uhbif19
# Formalization of matching logic (logic behind K Framework)

(Asked by: username_0 on 2023-07-16)

Is there any mechanization for matching logic (any flavor)?

I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the framework.

**Tags:** fl.formal-languages, coq, formal-methods, operational-semantics, agda


---

## 3 answers

### Answer by username_2 on 2023-08-15. Score: 6 | Accepted answer

There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of any formalization covering completeness of matching logic (although there is a pen-and-paper proof in [Matching μ-Logic](https://doi.org/10.1109/LICS.2019.8785675), and a [master's thesis](https://is.muni.cz/th/mcbtk/thesis.pdf)).

# [Applicative Matching Logic in Coq](https://github.com/harp-project/AML-Formalization)

This formalization is still under development; [here is a paper about an earlier (middle of 2022) version of it](https://doi.org/10.4204/EPTCS.369.2).
The current version covers:

* Syntax (using the locally nameless encoding of binders) including mu; semantics; proof system.
* Soundness of the proof system.
* A "proof mode" on top of the proof system - a set of tactics for constructing matching logic proofs interactively.
* Theory of definedness/equality (both from a model-theoretical and proof-theoretical perspective).
* Theory of sorts and natural numbers.
* Many proof system theorems from [Matching μ-Logic](https://doi.org/10.1109/LICS.2019.8785675), adapted to AML.
* Deduction theorem - a proof (of the most general variant available in a [technical report](http://hdl.handle.net/2142/102281) accompanying the above-linked Matching μ-Logic paper), as well as an infrastructure for using that theorem.
* Some other model theory (isomorphisms, "model extension").

# [Applicative Matching Logic in Lean](https://gitlab.com/ilds/aml-lean/MatchingLogic)

* Syntax (using named encoding of binders) including mu; semantics; proof system.
* Soundness of the proof system.
* [Proof extraction into Metamath](https://gitlab.com/ilds/aml-lean/AML-Lean-to-Metamath) (see the Metamath-based formalization below).
* Deduction theorem for closed patterns.

# [Applicative Matching Logic in Metamath](https://github.com/runtimeverification/proof-generation/blob/main/theory/matching-logic.mm)

Introduced for [proof object generation for the K Framework](https://doi.org/10.1007/978-3-030-81688-9_23).

* Syntax (using named encoding of binders) including mu.
* Proof system.
* Lots of lemmas using the proof system.

# [A Translator from K into Dedukti](https://gitlab.com/semantiko/kamelo)

> **Comments:**
> **username_3**: Note that the Metamath proof generation includes a translation from K's kore to Matching Logic. Unfortunately it is not too well documented.   https://github.com/runtimeverification/proof-generation/tree/main/src/proof_generation/kore  

---

### Answer by username_1 on 2023-08-16. Score: 1

I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti.

More precisely, my work focuses on:

* The translation from K into Dedukti that you mention (probably because you found this paper: <https://doi.org/10.4230/LIPIcs.TYPES.2022.12>) is based on the translation from K into Matching Logic. Your translation interprets the Matching Logic operators to be able to execute programs into Dedukti.
* A shallow encoding from Matching mu-Logic is available here: <https://gitlab.com/semantiko/ML2DK> (need to be updated). This encoding is a first step to recheck KProver proofs into Dedukti.

The encodings of Applicative Matching Logic (AML) into Lean and Coq are deep and they want to formalize theoretical results about AML.

Could you tell us why you are interested in mechanizing Matching Logic?
The various projects carried out to formalize Matching Logic are not of the same nature, and do not involve the same version of Matching Logic.

> **Comments:**
> **username_0**: I am interested for several reasons. 1. To understand matching logic better (cuz it is not very clear, which statements on that are proved, and how it compares to more well known logics) 2. To understand how (parametrized?) soundess/completeness usually look.  
> **username_0**: Your work direction is very interesting BTW, I was heard of it before.  

---

### Answer by username_0 on 2023-07-16. Score: 0

Okay, I need to admit that I am not best at googling. It already exists. Seems like the soundness is covered, and completeness only covered for non-mu part.

<https://arxiv.org/abs/2201.05716>

As for applicative version of matching logic, I did not find anything.


---

