Matching µ-logic: Foundation of K framework

DOI10.4230/LIPICS.CALCO.2019.1MaRDI QIDQ5875341zbMATH OpenOpenAlexFDO

Authors

Publication date 3 February 2023

Full work available at URL https://experts.illinois.edu/en/publications/matching-µ-logic-foundation-of-k-framework

zbMATH Keywords

matching \(\mu\)-logicprogram verificationreachability logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Matching logic -- extended abstract (invited talk)
• scientific article; zbMATH DE number 4208060
• \(\in_\mu\)-logic -- a theory of propositional logics
• Approximations of modal logics: K and beyond
• MV-algebras: An approach to fixed points in Łukasiewicz logic
• Modal logics and mu-calculi: An introduction
• scientific article; zbMATH DE number 3893173
• k-transforms in classical and paraconsistent logics
• Matching topological and frame products of modal logics
• An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework

Cites work

• An axiomatic basis for computer programming
• scientific article; zbMATH DE number 3799616 (Why is no real title available?)
• K-Java: a complete semantics of Java
• Matching logic
• One-path reachability logic

Cited in

(7)

• An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
• A matching logic foundation for Alk
• Towards a unifying logical framework for neural networks
• Interactive matching logic proofs in Coq
• Proof-carrying parameters in certified symbolic execution
• Difference of constrained patterns in logically constrained term rewrite systems
• Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms

Describes a project that uses

Uses Software

• K-Java
• KJS

This page was built for publication: Matching µ-logic: Foundation of K framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875341)