Prepas.org

Le site de l'UPS pour les Classes Préparatoires aux Grandes Écoles

Introduction à l'assistant de preuve Coq

David Cachera et David Pichardie (ENS Rennes, IRISA / INRIA Rennes) ont proposé une introduction à l'assistant de preuve Coq.

  • Certification de logiciel ;
  • vérification d'un mini compilateur en Coq.


Le logiciel est téléchargeable ici

Les documents utilisés pendant les séances peuvent être téléchargés ici ou en bas de cette page.