Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- 12 Separation logic as a logic
- 13 From separation algebras to separation logic
- 14 Simplification by rewriting
- 15 Introduction to step-indexing
- 16 Predicate implication and subtyping
- 17 General recursive predicates
- 18 Case study: Separation logic with first-class functions
- 19 Data structures in indirection theory
- 20 Applying higher-order separation logic
- 21 Lifted separation logics
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
13 - From separation algebras to separation logic
from II - Higher order separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- 12 Separation logic as a logic
- 13 From separation algebras to separation logic
- 14 Simplification by rewriting
- 15 Introduction to step-indexing
- 16 Predicate implication and subtyping
- 17 General recursive predicates
- 18 Case study: Separation logic with first-class functions
- 19 Data structures in indirection theory
- 20 Applying higher-order separation logic
- 21 Lifted separation logics
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
Summary
Predicates (of type A → Prop) in type theory give a model for Natural Deduction. A separation algebra gives a model for separation logic. We formalize these statements in Coq.
For a more expressive logic that permits general recursive types and quasi-self-reference, we use step-indexed models built with indirection theory. We will explain this in Part V; for now it suffices to say that indirection theory requires that the type T be ageable—elements of T must contain an approximation index. A given element of the model contains only a finite approximation to some ideal predicate; these approximations become weaker as we “age” them—which we do as the some operational semantics takes its steps.
To enforce that T is ageable we have a typeclass, ageable(T). Furthermore, when Separation is involved, the ageable mechanism must be compatible with the separating conjunction; this requirement is also expressed by a typeclass, Age_alg(T).
Theorem: Separation Algebras serve as a model of Separation Logic.
Proof. We express this theorem in Coq by saying that given type T, the function algNatDed models an instance of NatDed(pred T). Given a SepAlg over T, the function algSepLog models an instance of SepLog(pred T). The definability of algNatDed and algSepLog serve as a proof of the theorem.
What we show in this chapter is the indirection theory version (in the Coq file msl/alg_seplog.v), so ageable and Age-alg are mentioned from time to time.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 84 - 88Publisher: Cambridge University PressPrint publication year: 2014