Volume 3: Verified Functional Algorithms
Demonstration of how a variety of fundamental data structures can be specified and verified.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Volume 5: Verifiable C softwarefoundations.cis.upenn.edu
An extended tutorial on specifying and verifying C programs using the Verified Software Toolchain.
-
Volume 1: Logical Foundations softwarefoundations.cis.upenn.edu
Introduction to functional programming, basic concepts of logic, and computer-assisted theorem proving.
-
Functional Algorithms Verified in SSReflect github.com
Purely functional verified implementations of algorithms for searching, sorting, and other fundamental problems.
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
-
Volume 6: Separation Logic Foundations softwarefoundations.cis.upenn.edu
An introduction to separation logic and how to build program verification tools on top of it.
-
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.
Coq › Resources > Books: “Demonstration of how a variety of fundamental data structures can be specified and verified.”