Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- 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
5 - Mechanized Semantic Library
from I - Generic separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- 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
In constructing program logics for particular applications, for particular languages, 20th-century scientists had particular difficulty with pointers—aliasing and antialiasing, updates to state, commuting of operators; and self-reference—recursive functions, recursive types, functions as first-class values, types and predicates as parameters to functions. The combination of these two was particularly difficult: pointers to mutable records that can contain pointers to function-values that operate on mutable records.
Two strains of late-20th-century logic shed light on these matters.
Girard's 1987 linear logic [43] and other substructural logics treat logical assertions as resources that can be created, consumed and (when necessary) duplicated. This kind of thinking led to the Ishtiaq/O'Hearn/Reynolds invention in 2001 of separation logic [56, 79], which is a substructural Hoare logic for reasoning about sharing and antialiasing in pointer-manipulating programs.
Scott's 1976 domain theory [84] treats data types as approximations, thereby avoiding paradoxes about recursive types and other recursive definitions/specifications: a type can be defined in terms of more approximate versions of itself, which eventually bottoms out in a type that contains no information at all. These ideas led to the Appel/McAllester/Ahmed invention in 2001 of step-indexing [10, 2] which is a kind of practical domain theory for computations on von Neumann machines.
Many 21st-century scientists have generalized these methods for application to many different program logics (and other applications); and have formalized these methods within mechanical proof assistants.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 33 - 34Publisher: Cambridge University PressPrint publication year: 2014