Development of Correct-by-Construction Functional Parallel Programs

Instructor

• Frédéric Loulergue

Slides and Source Code

• Slides
• Source Code:
  • Introduction.v
  • Programming.v
  • Proofs.v

Virtual Machine

Virtual Machine for Virtual Box (or another hypervisor) containing the following tools:

• Coq version 8.4pl6
• OCaml version 4.02
• BSML version 0.5.4
• SyDPaCC
• Emacs and Proof General
• An MPI Libraray

The Virtual Machine. The password of user is user.