Volume 6: Separation Logic Foundations
An introduction to separation logic and how to build program verification tools on top of it.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Foundations of Separation Logic chargueraud.org
Introduction to using separation logic to reason about sequential imperative programs in Coq.
-
Volume 1: Logical Foundations softwarefoundations.cis.upenn.edu
Introduction to functional programming, basic concepts of logic, and computer-assisted theorem proving.
-
Program Logics for Certified Compilers cs.princeton.edu
Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.
-
Volume 2: Programming Language Foundations softwarefoundations.cis.upenn.edu
Introduction to the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
-
-
Software Foundations softwarefoundations.cis.upenn.edu
Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
Coq › Resources > Books: “An introduction to separation logic and how to build program verification tools on top of it.”