Assia Mahboubi

According to our database, Assia Mahboubi authored at least 40 papers between 2005 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Machine-Checked Categorical Diagrammatic Reasoning.

Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez

CoRR, 2024

Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence.

Cyril Cohen, Enzo Crance, Assia Mahboubi

Proceedings of the Programming Languages and Systems, 2024

Trocq: Proof Transfer for Free, With or Without Univalence.

Cyril Cohen, Enzo Crance, Assia Mahboubi

Proceedings of the Programming Languages and Systems, 2024

A First Order Theory of Diagram Chasing.

Assia Mahboubi, Matthieu Piquerez

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

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

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Machine-Checked Computational Mathematics (Invited Talk).

Assia Mahboubi

Proceedings of the 10th Conference on Algebra and Coalgebra in Computer Science, 2023

2022

Modular 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

CoRR, 2022

Gardening with the Pythia A Model of Continuity in a Dependent Setting.

Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot

Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, 2022

2021

A Formal Proof of the Irrationality of ζ(3).

Assia Mahboubi, Thomas Sibut-Pinote

Log. Methods Comput. Sci., 2021

Unsolvability of the Quintic Formalized in Dependent Type Theory.

Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Mathematical Structures in Dependent Type Theory (Invited Talk).

Assia Mahboubi

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Machine-checked computer-aided mathematics.

Assia Mahboubi

, 2021

2020

Preface: Selected Extended Papers from Interactive Theorem Proving 2018.

Jeremy Avigad, Assia Mahboubi

J. Autom. Reason., 2020

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

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Formally Verified Approximations of Definite Integrals.

Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote

J. Autom. Reason., 2019

A Certificate-Based Approach to Formally Verified Approximations.

Florent Bréhard, Assia Mahboubi, Damien Pous

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

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

Erratum to: Interactive Theorem Proving.

Jeremy Avigad, Assia Mahboubi

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

An induction principle over real numbers.

Assia Mahboubi

Arch. Math. Log., 2017

2015

Axiomatic Constraint Systems for Proof Search Modulo Theories.

Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

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

A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3).

Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Computer-checked mathematics: a formal proof of the odd order theorem.

Assia Mahboubi

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

The Rooster and the Butterflies.

Assia Mahboubi

Proceedings of the Intelligent Computer Mathematics, 2013

A bisimulation between DPLL(<i>T</i>) and a proof-search strategy for the focused sequent calculus.

Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Canonical Structures for the Working Coq User.

Assia Mahboubi, Enrico Tassi

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

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, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Two simulations about DPLL(T)

Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi

CoRR, 2012

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

Cyril Cohen, Assia Mahboubi

Log. Methods Comput. Sci., 2012

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

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

A formal study of Bernstein coefficients and polynomials.

Yves Bertot, Frédérique Guilhot, Assia Mahboubi

Math. Struct. Comput. Sci., 2011

2010

An introduction to small scale reflection in Coq.

Georges Gonthier, Assia Mahboubi

J. Formaliz. Reason., 2010

A Formal Quantifier Elimination for Algebraically Closed Fields.

Cyril Cohen, Assia Mahboubi

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Packaging Mathematical Structures.

François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2007

Implementing the cylindrical algebraic decomposition within the Coq system.

Assia Mahboubi

Math. Struct. Comput. Sci., 2007

A Modular Formalisation of Finite Group Theory.

Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

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

PhD thesis, 2006

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials.

Assia Mahboubi

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Proving Equalities in a Commutative Ring Done Right in Coq.

Benjamin Grégoire, Assia Mahboubi

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Programming and certifying a CAD algorithm in the Coq system.

Assia Mahboubi

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005