First-order hybrid separation logic

DOI10.1007/S10817-025-09739-4MaRDI QIDQ6912392zbMATH OpenFDO

Authors Frank S. de Boer, Hans-Dieter A. Hiep

Publication date 22 October 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09739-4

zbMATH Keywords

natural deductionseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• 30 years of research and development around Coq
• A complete axiomatisation for quantifier-free separation logic
• A decision procedure for separation logic in SMT
• Completeness for a first-order abstract separation logic
• Completeness in the theory of types
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• On the almighty wand
• Parametric completeness for separation theories
• Permission accounting in separation logic
• Tableaux and resource graphs for separation logic
• The completeness of the first-order functional calculus
• The logic of separation logic: models and proofs
• The semantics and proof theory of the logic of bunched implications

This page was built for publication: First-order hybrid separation logic

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