CompCert pour les nuls

Une introduction à la compilation formellement vérifiée

Support de cours:

• Les transparents: pour présenter et pour imprimer (6 par page).
• Développement Coq sur le langage IMP, commenté, pour être vu en ligne:
  • IMP: syntaxe et sémantiques d'IMP.
  • IMPcompiler: compilation d'IMP vers une machine virtuelle, et sa preuve de correction.
  • Sequences: bibliothèque sur les séquences de transition et leurs propriétés.
• Développement Coq sur le langage IMP, distribution source: IMP.zip.
• CompCert: sources Coq commentées
• Petits programmes C pour expérimenter avec l'interprète de référence.

Textes de référence:

• PowerPC 32-bit programmer's manual
• ISO C 99 standard