Higher-Order Separation Logic in Isabelle/HOLCF

DOI10.1016/j.entcs.2008.10.022zbMath1286.68404OpenAlexW1963706207MaRDI QIDQ5415649

Carsten Varming, Lars Birkedal

Publication date: 13 May 2014

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.10.022

zbMATH Keywords

verificationreliabilityseparation logicIsabelle/HOLcopying garbage collection

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Some Domain Theory and Denotational Semantics in Coq ⋮ Proof tactics for assertions in separation logic ⋮ Frame rule for mutually recursive procedures manipulating pointers ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq

Uses Software

• Isabelle/HOL

Cites Work

• Unnamed Item
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Separation logic, abstraction and inheritance
• Local reasoning about a copying garbage collector
• HOLCF = HOL + LCF
• Computer Science Logic
• Programming Languages and Systems
• A nonrecursive list compacting algorithm
• Abstract Predicates and Mutable ADTs in Hoare Type Theory