Program Logics

github.comtool

Companion Coq sources for a course on program logics at Collège de France.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Mechanized Semantics github.com

   tool category #coq link ↗

   Companion Coq sources for a course on programming language semantics at Collège de France.

2. ▲
   Program verification with types and logic gitlab.science.ru.nl

   site category #coq link ↗

   Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.

   
3. ▲
   Program Logics for Certified Compilers cs.princeton.edu

   site category #coq link ↗

   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.

4. ▲
   Logics for Epistemic Programs link.springer.com

   site category #agi-cocosci link ↗

   Synthese, 2004. [All Versions].

   
5. ▲
   CFML gitlab.inria.fr

   site category #coq link ↗

   Tool for proving properties of OCaml programs in separation logic.

   
6. ▲
   Hybrid site.uottawa.ca

   site category #coq link ↗

   System for reasoning using higher-order abstract syntax representations of object logics.

Coq › Resources > Course Material: “Companion Coq sources for a course on program logics at Collège de France.”