Program logic and equivalence in the presence of garbage collection.

DOI10.1016/S0304-3975(02)00868-XMaRDI QIDQ1874283zbMATH OpenFDO

Authors Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat

Publication date 25 May 2003

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(02)00868-X

zbMATH Keywords

observational equivalence

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 1701349
• Local reasoning about a copying garbage collector
• scientific article; zbMATH DE number 1497827
• A semantics for concurrent separation logic
• A certified framework for compiling and executing garbage-collected languages

Cites work

• A variable typed logic of effects
• BI as an assertion language for mutable data structures
• scientific article; zbMATH DE number 3560698 (Why is no real title available?)
• scientific article; zbMATH DE number 1142325 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 1390329 (Why is no real title available?)
• scientific article; zbMATH DE number 3289430 (Why is no real title available?)
• Sheaves in geometry and logic: a first introduction to topos theory

Cited in

(9)

• Formally verifying exceptions for low-level code with separation logic
• Local local reasoning: a BI-hyperdoctrine for full ground store
• On assertion-based encapsulation for object invariants and simulations
• Specification and verification challenges for sequential object-oriented programs
• scientific article; zbMATH DE number 1701349 (Why is no real title available?)
• Garbage Collection for Reversible Functional Languages
• Local reasoning about a copying garbage collector
• scientific article; zbMATH DE number 1497827 (Why is no real title available?)
• Observational purity and encapsulation

This page was built for publication: Program logic and equivalence in the presence of garbage collection.

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