Formal Reasoning About Programs
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
- from
- Theoretical Computer Science, Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Volume 1: Logical Foundations softwarefoundations.cis.upenn.edu
Introduction to functional programming, basic concepts of logic, and computer-assisted theorem proving.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
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.
-
Program Logics github.com
Companion Coq sources for a course on program logics at Collège de France.
-
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.
-
Program verification with types and logic gitlab.science.ru.nl
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
Theoretical Computer Science › Formal Verification > Books: “A book introducing both machine-checked proof with Coq Proof Assistant and approaches to formal reasoning about program correctness.”
Coq › Resources > Books: “Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.”