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

• Zhenjiang Hu,  National Institute of Informatics and  IPL, The University of Tokyo
• Frédéric Loulergue,  LIFO,  Université d'Orléans
• Julien Tesson,  LIFO,  Université d'Orléans
• Sylvain Dailler,  LIFO,  Université d'Orléans
• Kimironi Matsuzaki,  Kochi University of Technology
• Masato Takeichi,  IPL, The University of Tokyo

Past members: Louis Gesbert, Hideki Hashimoto

Software

•  Library "Systematic Development of Parallel Programs" version 0.1
•  Library "Program Calculation in Coq" version 0.15
•  Library "Program Calculation in Coq" version 0.1

Publications

Journal and conferences

• J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. Program Calculation in Coq. In Thirteenth International Conference on Algebraic Methodology And Software Technology (AMAST2010), LNCS. Springer, 2010. to appear
• 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.

Research reports and thesis

• Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue and Louis Gesbert,  Systematic Development of Functional Bulk Synchronous Parallel Programs, Research Report RR-2010-01, LIFO, University of Orléans, 2010
• 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
• 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