Interactive matching logic proofs in Coq

DOI10.1007/978-3-031-47963-2_10MaRDI QIDQ6605348zbMATH OpenFDO

Authors Jan Tušil, Péter Bereczky, Dániel Horpácsi

Publication date 13 September 2024

Full work available at URL https://doi.org/10.1007/978-3-031-47963-2_10

zbMATH Keywords

Coqinteractive reasoningmatching logicsequent calculus

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A matching logic foundation for Alk
• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• Capturing constrained constructor patterns in matching logic
• Contraction-free sequent calculi for intuitionistic logic
• Formalized proof systems for propositional logic
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• Interactive proofs in higher-order concurrent separation logic
• Jape: a calculator for animating proof-on-paper
• Matching logic
• Matching logic explained
• Matching µ-logic: Foundation of K framework
• Practical Tactics for Separation Logic
• Separation Logic for Small-Step cminor
• The locally nameless representation
• Towards a trustworthy semantics-based language framework via proof generation

Cited in

(2)

• Unification and anti-unification in applicative matching logic
• Toward model-theoretic consistency verification in a dependently typed encoding of matching logic

This page was built for publication: Interactive matching logic proofs in Coq

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