Welcome to SyDPaCC Home Page

SyDPaCC is a framework for the Systematic Development of Programs of Parallel and Cloud Computing. We use the ​Coq proof assistant for systematically calculate Bulk Synchronous Parallel ML (or ​BSML) programs from specifications.

Team

• Frédéric Loulergue, ​SICCS, ​Northern Arizona University, USA
• Wadoud Bousdira, ​LIFO, ​Université d'Orléans, France
• Jolan Philippe, ​LIFO, ​Université d'Orléans, France
• Julien Tesson, ​LACL, ​Université Paris Est Créteil, France
• Chris Whitney, ​SICCS, ​Northern Arizona University, USA

Past members: Louis Gesbert, Hideki Hashimoto, Masato Takeichi, Sylvain Dailler, Vitor Rodrigues, Simon Robillard, Zhenjiang Hu, Virginia Niculescu, Kiminori Matsuzaki, Kento Emoto

Software

• A Virtual Machine containing Coq, CoqIDE, Emacs (Proof General and Company Coq), OCaml, BSML, and SyDPaCC version core-0.2pre ​sydpacc.ova used during an ​ACM SAC 2016 tutorial
• The SyDPaCC Framework: ​version core-0.2, ​version Core-0.1beta (​EJC-IM version), ​version ITP2014, ​version Jan2014 (requires ​BSML for compiling parallel programs)
• Library "Systematic Development of Parallel Programs" ​version 0.1, ​version nii2013 (includes CertifiedBSML version nii2013, ProgramCalculationInCoq version 0.16, LIFO)
• Library "Program Calculation in Coq": ​version 0.1, ​version 0.15, ​version 0.16 (for Coq 8.3), ​version nii2013 (for Coq 8.4)

Publications

Journal

• Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. Int J Parallel Prog, 2016. ​doi:10.1007/s10766-016-0415-8
  Version of SyDPaCC related to this paper: ​version core-0.2pre. ​Experiments about the maximum prefix sum application.

Book Chapter

• Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq. In Nicolas Ollinger, editor, Informatique Mathématique, collection Alpha. CNRS Éditions, pages 87-134, 2015. (Tutorial for the EJC-IM Spring School, in French).

Conferences

• Kento Emoto, Frédéric Loulergue, and Julien Tesson. ​A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. In ITP, number 8558 in LNAI, pages 258-274. Springer, 2014.
• Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, and Zhenjiang Hu. ​Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem. In ACM Symposium on Applied Computing (SAC), pages 1577-1584. ACM Press, 2014
• Frédéric Loulergue, Virginia Niculescu, and Simon Robillard. ​Powerlists in Coq: Programming and Reasoning. In First International Symposium on Computing and Networking (CANDAR), pages 57-65. IEEE Computer Society, 2013
• Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. ​Programming with BSP Homomorphisms. In F. Wolf, B. Mohr, and D. Ney, editors, Euro-Par 2013 Parallel Processing, number 8097 in LNCS, pages 446-457. Springer, 2013
• J. Tesson and F. Loulergue. ​A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In 11th International Conference on Computational Science (ICCS 2011), Procedia Computer Science. pages 36-45, Elsevier, 2011.
• L. Gesbert, Z. Hu, F. Loulergue, K. Matsuzaki, and J. Tesson. ​Systematic Development of Correct Bulk Synchronous Parallel Programs. In The 11th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT). IEEE Computer Society, 2010.
• 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 6486, pages 163–179, Springer, 2010
• 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.

Tutorials

• Frédéric Loulergue, ​Development of Correct-by-Construction Functional Parallel Programs, Tutorial, ACM Symposium on Applied Computing, Pisa, Italy, April 2016
• Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq, ​Ecole des Jeunes Chercheur/se/s en Informatique Mathématique, Orléans, France, April 2015.
• Frédéric Loulergue and Julien Tesson, Certified Parallel Program Calculation in Coq, ​HPCS, Bologna, Italy, July 2014

Thesis

• Julien Tesson, ​Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels. PhD Thesis, LIFO, University of Orléans, November 2011
• 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

Research reports

• Frédéric Loulergue, Virginia Niculescu, ​Programming and Reasoning with PowerLists in Coq, Research Report RR-2013-02, LIFO, Université d'Orléans, 2013
• 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