2023

• Frédéric Loulergue and Ali Ed-Dbali. Verified high performance computing: the SyDPaCC approach. In 16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), LNCS. Springer, 2023, preprint, paper.
• Frédéric Loulergue and Jolan Philippe. Towards verified scalable parallel computing with Coq and Spark. In Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP), pages 11-17, New York, NY, USA, ACM, 2023, paper.

2019

• Jolan Philippe and Frédéric Loulergue. Parallel programming with Coq: Map and reduce skeletons on trees. In ACM Symposium on Applied Computing (SAC), pages 1578-1581. ACM, 2019, paper.

2017

• Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. Int J Parallel Prog, 45:300–319, 2017, paper.
• Frédéric Loulergue. A verified accumulate algorithmic skeleton. In Fifth International Symposium on Computing and Networking (CANDAR), pages 420-426, Aomori, Japan, November 19-22 2017. IEEE, paper.

2015

• Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq. In Nicolas Ollinger, editor, Informatique Mathématique une photographie en 2015, collection Alpha, pages 87–134. CNRS Éditions, 2015

2014

• Kento Emoto, Frédéric Loulergue, and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. In Interactive Theorem Proving (ITP), number 8558 in LNCS, pages 258–274, Wien, Austria, 2014. Springer. paper
• Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Légaux, 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, Gyeongju, Korea, ACM, 2014, paper.

2013

• Joeffrey Légaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Programming with BSP Homomorphisms. In Euro-Par Parallel Processing, number 8097 in LNCS, pages 446–457, Aachen, Germany, Springer, 2013, paper
• 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, Matsuyama, Japan, IEEE Computer Society, 2013, paper.

2012

• Wadoud Bousdira, Frédéric Loulergue, and Julien Tesson. A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays. In Algorithms and Architectures for Parallel Processing (ICA3PP), number 7439 in LNCS, pages 218–232, Fukuoka, Japan, Springer, 2012, paper

2011

• Julien Tesson and Frédéric Loulergue. A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In International Conference on Computational Science (ICCS), pages 36–45, Singapore, Elsevier, 2011, paper

2010

• Louis Gesbert, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Systematic Development of Correct Bulk Synchronous Parallel Programs. In Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 334–340. IEEE, 2010, paper
• Julien Tesson, H. Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program Calculation in Coq. In Algebraic Methodology And Software Technology (AMAST), LNCS 6486, pages 163–179. Springer, 2010, paper

2009

• H. Hashimoto, Zhenjiang Hu, Julien Tesson, Frédéric Loulergue, and Masato Takeichi. A Coq Library for Program Calculation. In JSSST Conference on Software Science and Technology, Shimane University, Shimane, Japan, 2009.