| 2026 | CPP | Certifying the Decidability of the Word Problem in Monoids at Large. | Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith |
| 2026 | ESOP | In Cantor Space No One Can Hear You Stream. | Martin Baillon, Assia Mahboubi, Pierre-Marie Pdrot |
| 2026 | FSCD | Not Choosing Is Still a Choice: Constructive mathematics without any choice. | Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, Pierre-Marie Pdrot |
| 2026 | ITP | Functional Correctness of an Optimized Modular Inversion Algorithm. | Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Toms Vallejos Parada |
| 2025 | FSCD | A Zoo of Continuity Properties in Constructive Type Theory. | Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pdrot, Matthieu Piquerez |
| 2024 | CSL | A First Order Theory of Diagram Chasing. | Assia Mahboubi, Matthieu Piquerez |
| 2024 | ESOP | Trocq: Proof Transfer for Free, With or Without Univalence. | Cyril Cohen, Enzo Crance, Assia Mahboubi |
| 2024 | ESOP | Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. | Cyril Cohen, Enzo Crance, Assia Mahboubi |
| 2024 | FSCD | Machine-Checked Categorical Diagrammatic Reasoning. | Benot Guillemet, Assia Mahboubi, Matthieu Piquerez |
| 2023 | CALCO | Machine-Checked Computational Mathematics (Invited Talk). | Assia Mahboubi |
| 2023 | CPP | Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. | Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial |
| 2022 | CSL | Gardening with the Pythia A Model of Continuity in a Dependent Setting. | Martin Baillon, Assia Mahboubi, Pierre-Marie Pdrot |
| 2021 | CSL | Mathematical Structures in Dependent Type Theory (Invited Talk). | Assia Mahboubi |
| 2021 | ITP | Unsolvability of the Quintic Formalized in Dependent Type Theory. | Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
| 2020 | CADE | Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. | Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi |
| 2019 | ITP | A Certificate-Based Approach to Formally Verified Approximations. | Florent Brhard, Assia Mahboubi, Damien Pous |
| 2018 | ITP | Erratum to: Interactive Theorem Proving. | Jeremy Avigad, Assia Mahboubi |
| 2016 | ITP | Formally Verified Approximations of Definite Integrals. | Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
| 2014 | CSL | Computer-checked mathematics: a formal proof of the odd order theorem. | Assia Mahboubi |
| 2014 | ITP | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). | Frdric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi |
| 2013 | ITP | A Machine-Checked Proof of the Odd Order Theorem. | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Franois Garillot, Stphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Thry |
| 2013 | ITP | Canonical Structures for the Working Coq User. | Assia Mahboubi, Enrico Tassi |
| 2012 | CADE | A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. | Franois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
| 2010 | AISC | A Formal Quantifier Elimination for Algebraically Closed Fields. | Cyril Cohen, Assia Mahboubi |
| 2006 | CADE | Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. | Assia Mahboubi |