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:

The semantics of an imperative language
- Module IMP: the imperative language IMP and its various semantics.
- Library Sequences: definitions and properties of reduction sequences.
Formal verification of a compiler
- Module Compil: compiling IMP to a virtual machine.
- Library Simulation: simulation diagrams between two transition systems.
Optimizations, static analyses, and their verification
- Module Optim: optimizations based on liveness analysis.
- Library Fixpoints: computing fixed points by Knaster-Tarski iteration.
Logics to reason about programs
- Module HoareLogic: Hoare logics for IMP
- Module SepLogic: a separation logic for IMP plus pointers and dynamic allocation.
Static analysis by abstract interpretation
- Module AbstrInterp: a static analyzer based on abstract interpretation.
- Module AbstrInterp2: improvements to the previous static analyzer.
Semantics of divergence
- Module Divergence: classical denotational semantics; coinductive natural semantics.
- Module Partiality: the partiality monad, with application to constructive denotational semantics.
Semantics and typing of a functional language
- Module FUN: the functional language FUN and its type system.

xavierleroy/cdf-mech-sem