Programming Languages and Systems

DOI10.1007/b107380zbMath1109.03021OpenAlexW4232919104MaRDI QIDQ5316567

Noah Torp-Smith, Bodil Biering, Lars Birkedal

Publication date: 13 September 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b107380

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (18)

On models of higher-order separation logic ⋮ A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Symbolic execution proofs for higher order store programs ⋮ From IF to BI. A tale of dependence and separation ⋮ Caper ⋮ Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Blaming the client: on data refinement in the presence of pointers ⋮ Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Local local reasoning: a BI-hyperdoctrine for full ground store ⋮ Unnamed Item ⋮ Higher-Order Separation Logic in Isabelle/HOLCF ⋮ Step-Indexed Kripke Model of Separation Logic for Storable Locks ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION

This page was built for publication: Programming Languages and Systems