Skip to content

xavierleroy/cdf-sem-meca

master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.

About

Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published