Calcul de programmes parallèles en Coq
ECJ-IM 2015

Les intervenants

• Wadoud Bousdira
• Frédéric Loulergue
• Julien Tesson

Le cours

• Le support de cours
• Le code source des exemples du cours :
  • defInductiveTypes.v
  • progFonctionnelle.v
  • Insert_sort.v
  • ClassMonoid.v
  • Bmf.v
  • Parallelisation.v

Pour essayer les exemples du cours

À installer :

• Coq version 8.4 (également installable avec OPAM ou WODI, mais attention temps de compilation assez long si vous utilisez ces gestionnaires de paquets pour la première fois)
• Recommendé: emacs et ProofGeneral

Exercices débutants

Il suffit d'avoir une version de Coq installée et travailler sur le fichier : Beginners.v

Une versions du fichier, avec des preuves : Beginners_avec_preuves.v

Pour les derniers exemples du cours et le TP (niveaux intermédiaires et avancés)

Les logiciels à installer :

• SyDPaCC version Core-0.1beta.tar.gz
• (Optionnel) Pour compiler les programmes parallèles : Bulk Synchronous Parallel ML (BSML): version 0.5.4pre

Pour en apprendre plus

Systematic Development of Programs for Parallel and Cloud Computing