Assia Mahboubi

Publication Activity (10 Years)

Years Active: 2005-2024
Publications (10 Years): 20

Top Venues

ITP

CoRR

CSL

J. Autom. Reason.

University of Nice Sophia Antipolis, France (PHD)

Education History

University of Nice Sophia Antipolis, France

PHD

Publications

Assia Mahboubi, Matthieu Piquerez
A First Order Theory of Diagram Chasing. CSL (2024)
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. CPP (2023)
Cyril Cohen, Enzo Crance, Assia Mahboubi
Trocq: Proof Transfer for Free, With or Without Univalence. CoRR (2023)
Assia Mahboubi, Matthieu Piquerez
A First Order Theory of Diagram Chasing. CoRR (2023)
Assia Mahboubi
Machine-Checked Computational Mathematics (Invited Talk). CALCO (2023)
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
Modular pre-processing for automated reasoning in dependent type theory. CoRR (2022)
Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
Gardening with the Pythia A Model of Continuity in a Dependent Setting. CSL (2022)
Assia Mahboubi
Mathematical Structures in Dependent Type Theory (Invited Talk). CSL (2021)
Assia Mahboubi, Thomas Sibut-Pinote
A Formal Proof of the Irrationality of ζ(3). Log. Methods Comput. Sci. 17 (1) (2021)
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP (2021)
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. IJCAR (2) (2020)
Jeremy Avigad, Assia Mahboubi
Preface: Selected Extended Papers from Interactive Theorem Proving 2018. J. Autom. Reason. 64 (5) (2020)
Assia Mahboubi, Thomas Sibut-Pinote
A Formal Proof of the Irrationality of ζ(3). CoRR (2019)
Florent Bréhard, Assia Mahboubi, Damien Pous
A Certificate-Based Approach to Formally Verified Approximations. ITP (2019)
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
Formally Verified Approximations of Definite Integrals. J. Autom. Reason. 62 (2) (2019)
Andrej Bauer, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Assia Mahboubi
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Dagstuhl Reports 8 (8) (2018)
Jeremy Avigad, Assia Mahboubi
Erratum to: Interactive Theorem Proving. ITP (2018)
Assia Mahboubi
An induction principle over real numbers. Arch. Math. Log. 56 (1-2) (2017)
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
Formally Verified Approximations of Definite Integrals. ITP (2016)
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
Axiomatic Constraint Systems for Proof Search Modulo Theories. FroCos (2015)
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP (2014)
Assia Mahboubi
Computer-checked mathematics: a formal proof of the odd order theorem. CSL-LICS (2014)
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. CoRR (2014)
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi
) and a proof-search strategy for the focused sequent calculus. LFMTP (2013)
Assia Mahboubi
The Rooster and the Butterflies. MKM/Calculemus/DML (2013)
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
A Machine-Checked Proof of the Odd Order Theorem. ITP (2013)
Assia Mahboubi, Enrico Tassi
Canonical Structures for the Working Coq User. ITP (2013)
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
Two simulations about DPLL(T) CoRR (2012)
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR (2012)
Cyril Cohen, Assia Mahboubi
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination Log. Methods Comput. Sci. 8 (1) (2012)
Yves Bertot, Frédérique Guilhot, Assia Mahboubi
A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. 21 (4) (2011)
Cyril Cohen, Assia Mahboubi
A Formal Quantifier Elimination for Algebraically Closed Fields. AISC/MKM/Calculemus (2010)
Georges Gonthier, Assia Mahboubi
An introduction to small scale reflection in Coq. J. Formaliz. Reason. 3 (2) (2010)
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
Packaging Mathematical Structures. TPHOLs (2009)
Assia Mahboubi
Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. 17 (1) (2007)
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
A Modular Formalisation of Finite Group Theory. TPHOLs (2007)
Assia Mahboubi
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. IJCAR (2006)
Assia Mahboubi
Programming and certifying a CAD algorithm in the Coq system. Mathematics, Algorithms, Proofs (2005)
Benjamin Grégoire, Assia Mahboubi
Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs (2005)

Assia Mahboubi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Assia Mahboubi