| 2025 | SAC | A Mechanized Formalization of an FRP Language with Effects. | Jordan Ischard, Frdric Dabrowski, Jules Chouquet, Frdric Loulergue |
| 2024 | FASE | Combining Deductive Verification with Shape Analysis. | To Bernier, Yani Ziani, Nikolai Kosmatov, Frdric Loulergue |
| 2024 | ISoLA | SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs. | Frdric Loulergue, Jordan Ischard |
| 2024 | TAP | Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. | Yani Ziani, Nikolai Kosmatov, Frdric Loulergue, Daniel Gracia Prez |
| 2023 | FTfJP | Towards Verified Scalable Parallel Computing with Coq and Spark. | Frdric Loulergue, Jolan Philippe |
| 2023 | IFM | Towards Formal Verification of a TPM Software Stack. | Yani Ziani, Nikolai Kosmatov, Frdric Loulergue, Daniel Gracia Prez, To Bernier |
| 2023 | SEFM | Verified Scalable Parallel Computing with Why3. | Olivia Proust, Frdric Loulergue |
| 2023 | VECoS | Verified High Performance Computing: The SyDPaCC Approach. | Frdric Loulergue, Ali Ed-Dbali |
| 2020 | ENASE | Pattern-driven Design of a Multiparadigm Parallel Programming Framework. | Virginia Niculescu, Frdric Loulergue, Darius Bufnea, Adrian Sterca |
| 2020 | ENASE | Reflections on the Design of Parallel Programming Frameworks. | Virginia Niculescu, Adrian Sterca, Frdric Loulergue |
| 2020 | TAP | Verified Runtime Assertion Checking for Memory Properties. | Dara Ly, Nikolai Kosmatov, Frdric Loulergue, Julien Signoles |
| 2019 | ICA3PP | Automatic Optimization of Python Skeletal Parallel Programs. | Frdric Loulergue, Jolan Philippe |
| 2019 | ICFEM | A First Step in the Translation of Alloy to Coq. | Salwa Souaf, Frdric Loulergue |
| 2019 | PDCAT | New List Skeletons for the Python Skeleton Library. | Frdric Loulergue, Jolan Philippe |
| 2019 | SAC | Logic against ghosts: comparison of two proof approaches for a list module. | Allan Blanchard, Nikolai Kosmatov, Frdric Loulergue |
| 2019 | SAC | Parallel programming with Coq: map and reduce skeletons on trees. | Jolan Philippe, Frdric Loulergue |
| 2018 | UIC | Verified Programs for Frequent Itemset Mining. | Frdric Loulergue, Christopher D. Whitney |
| 2018 | UIC | Interactive Bulk Synchronous Parallel Functional Programming in a Browser. | Julien Tesson, Frdric Loulergue |
| 2018 | TAP | Ghosts for Lists: From Axiomatic to Executable Specifications. | Frdric Loulergue, Allan Blanchard, Nikolai Kosmatov |
| 2017 | ICCS | Replicated Synchronization for Imperative BSP Programs. | Arvid Jakobsson, Frdric Dabrowski, Wadoud Bousdira, Frdric Loulergue, Gatan Hains |
| 2017 | ICCS | Imperative BSPlib-style Communications in BSML. | Frdric Loulergue |
| 2017 | PDCAT | Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML. | Frdric Loulergue |
| 2017 | PDCAT | A Java Framework for High Level Parallel Programming Using Powerlists. | Virginia Niculescu, Frdric Loulergue, Darius Bufnea, Adrian Sterca |
| 2016 | ISSTA | A CHR-Based Solver for Weak Memory Behaviors. | Allan Blanchard, Nikolai Kosmatov, Frdric Loulergue |
| 2016 | SCAM | Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. | Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frdric Loulergue |
| 2015 | FMICS | A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. | Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frdric Loulergue |
| 2015 | SAC | Nested atomic sections with thread escape: compilation. | Frdric Dabrowski, Frdric Loulergue, Thomas Pinsard |
| 2015 | SECRYPT | Cloud Resources Placement based on Functional and Non-functional Requirements. | Asma Guesmi, Patrice Clemente, Frdric Loulergue, Pascal Berthom |
| 2014 | ICCS | Handling Data-skew Effects in Join Operations Using MapReduce. | Mohamad Al Hajj Hassan, Mostafa Bamha, Frdric Loulergue |
| 2014 | ITP | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. | Kento Emoto, Frdric Loulergue, Julien Tesson |
| 2014 | SAC | Nested atomic sections with thread escape: a formal definition. | Frdric Dabrowski, Frdric Loulergue, Thomas Pinsard |
| 2014 | SAC | Formal derivation and extraction of a parallel program for the all nearest smaller values problem. | Frdric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, Zhenjiang Hu |
| 2014 | SYNASC | Implementing Powerlists with Bulk Synchronous Parallel ML. | Frdric Loulergue, Virginia Niculescu, Julien Tesson |
| 2013 | EuroPar | Programming with BSP Homomorphisms. | Joeffrey Legaux, Zhenjiang Hu, Frdric Loulergue, Kiminori Matsuzaki, Julien Tesson |
| 2013 | ICCS | OSL: An Algorithmic Skeleton Library with Exceptions. | Joeffrey Legaux, Frdric Loulergue, Sylvain Jubertie |
| 2013 | PDCAT | Nested Atomic Sections with Thread Escape: An Operational Semantics. | Frdric Dabrowski, Frdric Loulergue, Thomas Pinsard |
| 2012 | ICA3PP | A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays. | Wadoud Bousdira, Frdric Loulergue, Julien Tesson |
| 2012 | ICA3PP | Experiments in Parallel Matrix Multiplication on Multi-core Systems. | Joeffrey Legaux, Sylvain Jubertie, Frdric Loulergue |
| 2011 | PACT | A Formal Programming Model of Orlans Skeleton Library. | Noman Javed, Frdric Loulergue |
| 2011 | PPAM | Verification of a Heat Diffusion Simulation Written with Orlans Skeleton Library. | Noman Javed, Frdric Loulergue |
| 2010 | PDCAT | Systematic Development of Correct Bulk Synchronous Parallel Programs. | Louis Gesbert, Zhenjiang Hu, Frdric Loulergue, Kiminori Matsuzaki, Julien Tesson |
| 2007 | PDCAT | Semantics of an Exception Mechanism for Bulk Synchronous Parallel ML. | Louis Gesbert, Frdric Loulergue |
| 2007 | PPAM | Divide-and-Conquer Parallel Programming with Minimally Synchronous Parallel ML. | Radia Benheddi, Frdric Loulergue |
| 2007 | PPAM | Formal Semantics of DRMA-Style Programming in BSPlib. | Julien Tesson, Frdric Loulergue |
| 2006 | CSR | Bulk Synchronous Parallel ML: Semantics and Implementation of the Parallel Juxtaposition. | Frdric Loulergue, Radia Benheddi, Frdric Gava, D. Louis-Rgis |
| 2005 | ICCS | Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. | Frdric Loulergue, Frdric Gava, David Billiet |
| 2005 | SNPD | Optimizing Bulk Synchronous Parallel ML. | Frdric Loulergue |
| 2004 | ICCS | Communication Primitives for Minimally Synchronous Parallel ML. | Frdric Loulergue |
| 2003 | EuroPar | Parallel Juxtaposition for Bulk Synchronous Parllel ML. | Frdric Loulergue |
| 2003 | ICCS | A Parallel Virtual Machine for Bulk Synchronous Parallel ML. | Frdric Gava, Frdric Loulergue |
| 2003 | ICCS | Parallel Superposition for Bulk Synchronous Parallel ML. | Frdric Loulergue |
| 2003 | PACT | A Polymorphic Type System for Bulk Synchronous Parallel ML. | Frdric Gava, Frdric Loulergue |
| 2003 | SNPD | Semantics of Minimally Synchronous Parallel ML. | Myrto Arapinis, Frdric Loulergue, Frdric Gava, Frdric Dabrowski |
| 2003 | SNPD | A Parallel Categorical Abstract Machine for Bulk Synchronous Parallel ML. | Frdric Gava, Frdric Loulergue, Frdric Dabrowski |
| 2003 | SNPD | Pattern Matching of Parallel Values in Bulk Synchronous Parallel ML. | Frdric Gava, Frdric Loulergue, Frdric Dabrowski |
| 1997 | EuroPar | Functional Parallel Programming with Explicit Processes: Beyond SPMD. | Frdric Loulergue, Gatan Hains |