[[Image(sydpacc.png, nolink, right)]] = Welcome to SyDPaCC Home Page = SyDPaCC is a framework for the Systematic Development of Programs of Parallel and Cloud Computing. We use the [http://coq.inria.fr Coq] proof assistant for systematically calculate Bulk Synchronous Parallel ML (or [https://traclifo.univ-orleans.fr/BSML BSML]) programs from specifications. == Team == * Frédéric Loulergue, [http://www.nau.edu/SICCS SICCS], [http://www.nau.edu Northern Arizona University], USA * Wadoud Bousdira, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans], France * Jolan Philippe, [http://www.univ-orleans.fr/lifo LIFO], [http://www.univ-orleans.fr Université d'Orléans], France * Julien Tesson, [http://lacl.u-pec.fr/ LACL], [http://www.u-pec.fr Université Paris Est Créteil], France * Chris Whitney, [http://www.nau.edu/SICCS SICCS], [http://www.nau.edu 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 [http://frederic.loulergue.eu/sac2016/sydpacc.ova sydpacc.ova] used during an [http://frederic.loulergue.eu/sac2016 ACM SAC 2016 tutorial] * The '''SyDPaCC''' Framework: [http://frederic.loulergue.eu/ftp/sydpacc-core-0.2.tar.gz version core-0.2], [http://frederic.loulergue.eu/ftp/SyDPaCC-Core-0.1beta.tar.gz version Core-0.1beta] ([http://www.univ-orleans.fr/lifo/evenements/EJCIM2015 EJC-IM] version), [http://frederic.loulergue.eu/ftp/SyDPaCC-ITP2014.tar.bz2 version ITP2014], [http://frederic.loulergue.eu/ftp/SyDPaCC-Jan2014.tar.bz2 version Jan2014] (requires [http://traclifo.univ-orleans.fr/BSML BSML] for compiling parallel programs) * Library "Systematic Development of Parallel Programs" [http://frederic.loulergue.eu/ftp/sdpp-0.1.tar.bz2 version 0.1], [http://frederic.loulergue.eu/ftp/SDPP-nii2013.tar.bz2 version nii2013] (includes CertifiedBSML version nii2013, !ProgramCalculationInCoq version 0.16, LIFO) * Library "Program Calculation in Coq": [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.1.tar.bz2 version 0.1], [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.15.tar.bz2 version 0.15], [http://frederic.loulergue.eu/ftp/ProgramCalculationInCoq-0.16.tar.bz2 version 0.16] (for Coq 8.3), [https://traclifo.univ-orleans.fr/SDPP/raw-attachment/wiki/WikiStart/ProgramCalculationInCoq-nii2013.tar.gz 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. [http://dx.doi.org/10.1007/s10766-016-0415-8 doi:10.1007/s10766-016-0415-8] [[BR]] Version of SyDPaCC related to this paper: [http://frederic.loulergue.eu/ftp/sydpacc-core-0.2pre.tar.gz version core-0.2pre]. [https://traclifo.univ-orleans.fr/SyDPaCC/raw-attachment/wiki/WikiStart/mps_experiments.pdf 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. [http://dx.doi.org/10.1007/978-3-319-08970-6_17 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. [http://dx.doi.org/10.1145/2554850.2554912 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. [http://dx.doi.org/10.1109/CANDAR.2013.17 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. [http://dx.doi.org/10.1007/978-3-642-40047-6_46 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. [http://dx.doi.org/10.1016/j.procs.2011.04.005 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. [http://doi.ieeecomputersociety.org/10.1109/PDCAT.2010.86 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. [http://dx.doi.org/10.1007/978-3-642-17796-5_10 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. [http://frederic.loulergue.eu/ftp/hashimoto_hu_tesson_loulergue_takeichi_jssst2009.pdf A Coq Library for Program Calculation]. In JSSST Conference on Software Science and Technology, 2009. === Tutorials === * Frédéric Loulergue, [http://www.acm.org/conferences/sac/sac2016/tutorials.html 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, [http://www.univ-orleans.fr/lifo/evenements/EJCIM2015/ 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, [http://hpcs2014.cisedu.info/4-program/tutorials HPCS], Bologna, Italy, July 2014 === Thesis === * Julien Tesson, [ftp://ftp.univ-orleans.fr/theses/julien.tesson_2187.pdf 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, [http://tel.archives-ouvertes.fr/docs/00/48/13/76/PDF/2009PEST0004_0_1.pdf 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, [http:// 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, [http://hal.inria.fr/docs/00/46/61/83/PDF/RR-2010-01.pdf 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, [http://frederic.loulergue.eu/ftp/RR-2009-07.pdf Program Calculation in Coq], Research Report RR-2009-07, LIFO, University of Orléans, 2009