Programming and certifying a CAD algorithm in the Coq system. - Assia Mahboubi (Mathematics, Algorithms, Proofs, 2005)

Proving Equalities in a Commutative Ring Done Right in Coq. - Benjamin Grégoire; Assia Mahboubi (TPHOLs, 2005)

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. - Assia Mahboubi (IJCAR, 2006)

Contributions à la certification des calculs dans R : théorie, preuves, programmation. (Contributions to the certification of computations in R : theory, proofs, implementation). - Assia Mahboubi (2006)

A Modular Formalisation of Finite Group Theory. - Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry (TPHOLs, 2007)

Implementing the cylindrical algebraic decomposition within the Coq system. - Assia Mahboubi (Math. Struct. Comput. Sci., 2007)

Packaging Mathematical Structures. - François Garillot; Georges Gonthier; Assia Mahboubi; Laurence Rideau (TPHOLs, 2009)

A Formal Quantifier Elimination for Algebraically Closed Fields. - Cyril Cohen; Assia Mahboubi (AISC/MKM/Calculemus, 2010)

An introduction to small scale reflection in Coq. - Georges Gonthier; Assia Mahboubi (J. Formaliz. Reason., 2010)

A formal study of Bernstein coefficients and polynomials. - Yves Bertot; Frédérique Guilhot; Assia Mahboubi (Math. Struct. Comput. Sci., 2011)

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. - François Bobot; Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala; Assia Mahboubi; Alain Mebsout; Guillaume Melquiond (IJCAR, 2012)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination - Cyril Cohen; Assia Mahboubi (Log. Methods Comput. Sci., 2012)

Two simulations about DPLL(T) - Mahfuza Farooque; Stéphane Lengrand; Assia Mahboubi (CoRR, 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Canonical Structures for the Working Coq User. - Assia Mahboubi; Enrico Tassi (ITP, 2013)

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. - Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi (LFMTP, 2013)

The Rooster and the Butterflies. - Assia Mahboubi (MKM/Calculemus/DML, 2013)

Computer-checked mathematics: a formal proof of the odd order theorem. - Assia Mahboubi (CSL-LICS, 2014)

A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). - Frédéric Chyzak; Assia Mahboubi; Thomas Sibut-Pinote; Enrico Tassi (ITP, 2014)

Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. - Damien Rouhling; Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi; Jean-Marc Notin (CoRR, 2014)

Axiomatic Constraint Systems for Proof Search Modulo Theories. - Damien Rouhling; Mahfuza Farooque; Stéphane Graham-Lengrand; Assia Mahboubi; Jean-Marc Notin (FroCos, 2015)

An induction principle over real numbers. - Assia Mahboubi (Arch. Math. Log., 2017)

Erratum to: Interactive Theorem Proving. - Jeremy Avigad; Assia Mahboubi (ITP, 2018)

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). - Andrej Bauer; Martín Hötzel Escardó; Peter LeFanu Lumsdaine; Assia Mahboubi (Dagstuhl Reports, 2018)

A Certificate-Based Approach to Formally Verified Approximations. - Florent Bréhard; Assia Mahboubi; Damien Pous (ITP, 2019)

Formally Verified Approximations of Definite Integrals. - Assia Mahboubi; Guillaume Melquiond; Thomas Sibut-Pinote (J. Autom. Reason., 2019)

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 (IJCAR (2), 2020)

Preface: Selected Extended Papers from Interactive Theorem Proving 2018. - Jeremy Avigad; Assia Mahboubi (J. Autom. Reason., 2020)

Machine-checked computer-aided mathematics. - Assia Mahboubi (2021)

Mathematical Structures in Dependent Type Theory (Invited Talk). - Assia Mahboubi (CSL, 2021)

Unsolvability of the Quintic Formalized in Dependent Type Theory. - Sophie Bernard; Cyril Cohen; Assia Mahboubi; Pierre-Yves Strub (ITP, 2021)

A Formal Proof of the Irrationality of ζ(3). - Assia Mahboubi; Thomas Sibut-Pinote (Log. Methods Comput. Sci., 2021)

Gardening with the Pythia A Model of Continuity in a Dependent Setting. - Martin Baillon; Assia Mahboubi; Pierre-Marie Pédrot (CSL, 2022)

Modular pre-processing for automated reasoning in dependent type theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CoRR, 2022)

Machine-Checked Computational Mathematics (Invited Talk). - Assia Mahboubi (CALCO, 2023)

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CPP, 2023)

A First Order Theory of Diagram Chasing. - Assia Mahboubi; Matthieu Piquerez (CSL, 2024)

Trocq: Proof Transfer for Free, With or Without Univalence. - Cyril Cohen; Enzo Crance; Assia Mahboubi (ESOP (1), 2024)

Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. - Cyril Cohen; Enzo Crance; Assia Mahboubi (ESOP (1), 2024)

Machine-Checked Categorical Diagrammatic Reasoning. - Benoît Guillemet; Assia Mahboubi; Matthieu Piquerez (FSCD, 2024)

A Zoo of Continuity Properties in Constructive Type Theory. - Martin Baillon; Yannick Forster 002; Assia Mahboubi; Pierre-Marie Pédrot; Matthieu Piquerez (FSCD, 2025)