Mechanized semantics: the Coq development

This repository contains the Coq sources for the course "Mechanized semantics" given by Xavier Leroy at Collège de France in 2019-2020.

This is the English version of the Coq sources. La version commentée en français est disponible ici.

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

1. The semantics of an imperative language

   • Module IMP: the imperative language IMP and its various semantics.
   • Library Sequences: definitions and properties of reduction sequences.

2. Formal verification of a compiler

   • Module Compil: compiling IMP to a virtual machine.
   • Library Simulation: simulation diagrams between two transition systems.

3. Optimizations, static analyses, and their verification

   • Module Optim: optimizations based on liveness analysis.
   • Library Fixpoints: computing fixed points by Knaster-Tarski iteration.

4. Logics to reason about programs

   • Module HoareLogic: Hoare logics for IMP
   • Module SepLogic: a separation logic for IMP plus pointers and dynamic allocation.

5. Static analysis by abstract interpretation

   • Module AbstrInterp: a static analyzer based on abstract interpretation.
   • Module AbstrInterp2: improvements to the previous static analyzer.

6. Semantics of divergence

   • Module Divergence: classical denotational semantics; coinductive natural semantics.
   • Module Partiality: the partiality monad, with application to constructive denotational semantics.

7. Semantics and typing of a functional language

   • Module FUN: the functional language FUN and its type system.