Interactive matching logic proofs in Coq
From MaRDI portal
Publication:6605348
DOI10.1007/978-3-031-47963-2_10MaRDI QIDQ6605348
Péter Bereczky, Jan Tušil, Dániel Horpácsi
Publication date: 13 September 2024
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards a trustworthy semantics-based language framework via proof generation
- The locally nameless representation
- Matching logic explained
- Capturing constrained constructor patterns in matching logic
- Practical Tactics for Separation Logic
- Separation Logic for Small-Step cminor
- Contraction-free sequent calculi for intuitionistic logic
- Matching Logic
- An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
- Jape: A calculator for animating proof-on-paper
- Interactive proofs in higher-order concurrent separation logic
- Matching µ-logic: Foundation of K framework
- A matching logic foundation for Alk
This page was built for publication: Interactive matching logic proofs in Coq
