Matching mu-Logic: Foundation of K Framework (Invited Paper)
Chen, Xiaohong, Grigore Roşu · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2019
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.