We are announcing a new research project, continuing our partnership with Runtime Verification (RV). This project will further the Lean formalization of Matching Logic (ML) developed in the previous one, by establishing a link to the 𝕂 Semantic Framework. It will first formalize into Lean the theoretical foundation of 𝕂, i.e. Matching μ-Logic (μML), as well as implement a translator for specifications in KORE, the current intermediate representation for the 𝕂 language.
For more information, see the project page.