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

