Program logics: the companion Coq development

This repository contains Coq sources for the course "Program logics" given by Xavier Leroy at Collège de France in 2021.

This is work in progress.

An HTML pretty-printing of the commented sources is also available:

1. Variables and loops: Hoare logics

   • Module Hoare: Hoare logics for the imperative language IMP.
   • Library Sequences: definitions and properties of reduction sequences.

2. Pointers and data structures: separation logic

   • Module Seplog: separation logic for the functional/imperative language PTR.
   • Library Separation: definitions and properties of heaps and separation logic assertions.

3. Shared-memory concurrency: concurrent separation logic

   • Module CSL: concurrent separation logic for the PTR language + parallel and atomic constructs.

4. Hoare monads and Dijkstra monads

   • Module Monads
   • Library Delay (coinductive definition of possibly nonterminating computations).