Welcome to SDPP Home Page

SDPP is a framework for Systematic Development of Parallel Programs.

We use the  Coq proof assistant for systematically derive Bulk Synchronous Parallel ML (or  BSML) programs.

Team

• Hideki Hashimoto,  IPL, The University of Tokyo
• Zhenjiang Hu,  National Institute of Informatics and  IPL, The University of Tokyo
• Louis Gesbert,  LACL,  Université Paris Est Créteil and  MLstate
• Frédéric Loulergue,  LIFO,  Université d'Orléans
• Kimironi Matsuzaki,  Kochi University of Technology
• Masato Takeichi,  IPL, The University of Tokyo
• Julien Tesson,  LIFO,  Université d'Orléans

Software

•  Library "Program Calculation in Coq" version 0.1

Publications

• Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi,  Program Calculation in Coq, Research Report RR-2009-07, LIFO, University of Orléans, 2009
• H. Hashimoto, Z. Hu, J. Tesson, F. Loulergue, and M. Takeichi. A Coq Library for Program Calculation. In JSSST Conference on Software Science and Technology, 2009.
• Louis Gesbert, Développement systématique et sûreté d'exécution en programmation parallèle structurée. PhD thesis, University Paris Est, LACL, 2009