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
Last modified 17 months ago
Last modified on Feb 14, 2017, 11:48:06 PM
Attachments (3)
- sydpacc.png (157.7 KB) - added by frederic.loulergue@… 5 years ago.
- ProgramCalculationInCoq-nii2013.tar.gz (18.0 KB) - added by frederic.loulergue@… 5 years ago.
- mps_experiments.pdf (37.1 KB) - added by frederic.loulergue@… 3 years ago.
Download all attachments as: .zip