Awesome

Sémantiques mécanisées: le développement Coq

Ce dépôt contient les sources Coq pour le cours "Sémantiques mécanisées" de Xavier Leroy au Collège de France en 2019-2020.

Cette version est commentée en français. The English version is available here.

Un rendu HTML des sources commentés est également disponible:

1. La sémantique d'un langage impératif

   • Module IMP: le langage impératif IMP et ses sémantiques.
   • Bibliothèque Sequences: définitions et propriétés des suites de réductions.

2. Vérification formelle d'un compilateur

   • Module Compil: compilation de IMP vers une machine virtuelle.
   • Bibliothèque Simulation: diagrammes de simulation entre deux systèmes de transitions.

3. Optimisations, analyses statiques, et leur vérification

   • Module Optim: optimisations à base d'analyse de vivacité.
   • Bibliothèque Fixpoints: calcul de points fixes par itération de Knaster-Tarski.

4. Des logiques pour raisonner sur les programmes

   • Module HoareLogic: des logiques de Hoare faible et forte pour IMP.
   • Module SepLogic: une logique de séparation pour IMP plus pointeurs et allocation dynamique.

5. L'analyse statique par interprétation abstraite

   • Module AbstrInterp: un analyseur statique par interprétation abstraite.
   • Module AbstrInterp2: une amélioration de l'analyseur statique précédent.

6. Sémantiques de la divergence

   • Module Divergence: sémantique dénotationnelle classique, sémantique naturelle coinductive.
   • Module Partiality: monade de partialité et sémantique dénotationnelle constructive.

7. Sémantique et typage d'un langage fonctionnel

   • Module FUN: le langage fonctionnel FUN et son système de types.