K definitions as matching logic theories, formally

DOI10.1007/978-3-032-22730-0_10MaRDI QIDQ7317482zbMATH OpenFDO

Authors Xiaohong Chen, Horaţiu Cheval, Dorel Lucanu, Grigore Roşu

Publication date 24 August 2026

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-22730-0_10

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• A formally verified compiler back-end
• A matching logic theory of multi-hole contexts
• A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations
• All-path reachability logic
• scientific article; zbMATH DE number 1722718 (Why is no real title available?)
• scientific article; zbMATH DE number 3423547 (Why is no real title available?)
• K-Java: a complete semantics of Java
• Matching -logic
• Matching logic
• Matching logic explained
• One-path reachability logic
• Program verification by coinduction
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Refinement Calculus
• Semantics engineering with PLT Redex
• The revised report on the syntactic theories of sequential control and state
• Towards a trustworthy semantics-based language framework via proof generation

Cited in

(1)

• A matching logic theory of multi-hole contexts

This page was built for publication: \( \mathbb{K}\) definitions as matching logic theories, formally

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