Idempotent resources in separation logic. The heart of \texttt{core} in Iris

DOI10.1007/978-3-031-90897-2_3MaRDI QIDQ6889897zbMATH OpenFDO

Authors Daniel Gratzer, Mathias Adam Møller, Lars Birkedal

Publication date 4 December 2025

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

Cites work

• BI as an assertion language for mutable data structures
• Fictional separation logic
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Higher-order ghost state
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• On models of higher-order separation logic
• Permission accounting in separation logic
• Sheaves in geometry and logic: a first introduction to topos theory
• The essence of higher-order concurrent separation logic
• The Logic of Bunched Implications
• Views, compositional reasoning for concurrent programs

This page was built for publication: Idempotent resources in separation logic. The heart of \texttt{core} in Iris

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