Program verification with types and logic
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Program Logics github.com
Companion Coq sources for a course on program logics at Collège de France.
-
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.
-
Mechanized Semantics github.com
Companion Coq sources for a course on programming language semantics at Collège de France.
-
Formal Reasoning About Programs adam.chlipala.net
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
-
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.
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
Coq › Resources > Course Material: “Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.”