Skip to Main content Skip to Navigation
Journal articles

Separation Logic for Sequential Programs

Arthur Charguéraud 1
1 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of lambda-calculus, semantics and logics, and therefore should be accessible to a broad audience.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-03108936
Contributor : Arthur Charguéraud <>
Submitted on : Wednesday, January 13, 2021 - 3:01:00 PM
Last modification on : Monday, January 18, 2021 - 11:44:31 AM

File

seq_seplogic.pdf
Files produced by the author(s)

Identifiers

Citation

Arthur Charguéraud. Separation Logic for Sequential Programs. Proceedings of the ACM on Programming Languages, ACM, 2020, 4, ⟨10.1145/3408998⟩. ⟨hal-03108936⟩

Share

Metrics

Record views

17

Files downloads

22