/cdf-mech-sem

Coq development for the course "Mechanized semantics", Collège de France, 2019-2020

Primary LanguageCoqGNU Lesser General Public License v2.1LGPL-2.1

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.