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
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
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.