Assia Mahboubi

52 papers A 2B 17Journal 17Unranked 13

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Certifying the Decidability of the Word Problem in Monoids at Large. CPP Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith
2026	—	`conf`	In Cantor Space No One Can Hear You Stream. ESOP (1) Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
2025	B	`conf`	A Zoo of Continuity Properties in Constructive Type Theory. FSCD Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez
2025	J	`jnl`	Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence. ACM Trans. Program. Lang. Syst. Cyril Cohen, Enzo Crance, Assia Mahboubi
2024	B	`conf`	A First Order Theory of Diagram Chasing. CSL Assia Mahboubi, Matthieu Piquerez
2024	—	`conf`	Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. ESOP (1) Cyril Cohen, Enzo Crance, Assia Mahboubi
2024	B	`conf`	Machine-Checked Categorical Diagrammatic Reasoning. FSCD Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
2024	J	`jnl`	Machine-Checked Categorical Diagrammatic Reasoning. CoRR Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
2024	—	`conf`	Trocq: Proof Transfer for Free, With or Without Univalence. ESOP (1) Cyril Cohen, Enzo Crance, Assia Mahboubi
2023	J	`jnl`	A First Order Theory of Diagram Chasing. CoRR Assia Mahboubi, Matthieu Piquerez
2023	B	`conf`	Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. CPP Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
2023	B	`conf`	Machine-Checked Computational Mathematics (Invited Talk). CALCO Assia Mahboubi
2023	J	`jnl`	Trocq: Proof Transfer for Free, With or Without Univalence. CoRR Cyril Cohen, Enzo Crance, Assia Mahboubi
2022	B	`conf`	Gardening with the Pythia A Model of Continuity in a Dependent Setting. CSL Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
2022	J	`jnl`	Modular pre-processing for automated reasoning in dependent type theory. CoRR Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
2021	J	`jnl`	A Formal Proof of the Irrationality of ζ(3). Log. Methods Comput. Sci. Assia Mahboubi, Thomas Sibut-Pinote
2021	—	`book`	Machine-checked computer-aided mathematics. Assia Mahboubi
2021	B	`conf`	Mathematical Structures in Dependent Type Theory (Invited Talk). CSL Assia Mahboubi
2021	B	`conf`	Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
2020	—	`ed.`	25th International Conference on Types for Proofs and Programs, TYPES 2019, Oslo, Norway, June 11-14, 2019 TYPES Marc Bezem, Assia Mahboubi
2020	—	`conf`	Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. IJCAR (2) Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
2020	J	`jnl`	Preface: Selected Extended Papers from Interactive Theorem Proving 2018. J. Autom. Reason. Jeremy Avigad, Assia Mahboubi
2019	B	`conf`	A Certificate-Based Approach to Formally Verified Approximations. ITP Florent Bréhard, Assia Mahboubi, Damien Pous
2019	J	`jnl`	A Formal Proof of the Irrationality of ζ(3). CoRR Assia Mahboubi, Thomas Sibut-Pinote
2019	J	`jnl`	Formally Verified Approximations of Definite Integrals. J. Autom. Reason. Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
2019	B	`ed.`	Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 CPP Assia Mahboubi, Magnus O. Myreen
2018	B	`conf`	Erratum to: Interactive Theorem Proving. ITP Jeremy Avigad, Assia Mahboubi
2018	J	`jnl`	Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Dagstuhl Reports Andrej Bauer, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Assia Mahboubi
2018	B	`ed.`	Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings ITP Jeremy Avigad, Assia Mahboubi
2017	J	`jnl`	An induction principle over real numbers. Arch. Math. Log. Assia Mahboubi
2016	B	`conf`	Formally Verified Approximations of Definite Integrals. ITP Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
2015	—	`conf`	Axiomatic Constraint Systems for Proof Search Modulo Theories. FroCos Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
2014	B	`conf`	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
2014	J	`jnl`	Axiomatisation of constraint systems to specify a tableaux calculus modulo theories. CoRR Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin
2014	—	`conf`	Computer-checked mathematics: a formal proof of the odd order theorem. CSL-LICS Assia Mahboubi
2013	B	`conf`	A Machine-Checked Proof of the Odd Order Theorem. ITP 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
2013	—	`conf`	A bisimulation between DPLL( LFMTP Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi
2013	B	`conf`	Canonical Structures for the Working Coq User. ITP Assia Mahboubi, Enrico Tassi
2013	—	`conf`	The Rooster and the Butterflies. MKM/Calculemus/DML Assia Mahboubi
2012	A	`conf`	A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
2012	J	`jnl`	Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination Log. Methods Comput. Sci. Cyril Cohen, Assia Mahboubi
2012	J	`jnl`	Two simulations about DPLL(T) CoRR Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
2011	J	`jnl`	A formal study of Bernstein coefficients and polynomials. Math. Struct. Comput. Sci. Yves Bertot, Frédérique Guilhot, Assia Mahboubi
2010	—	`conf`	A Formal Quantifier Elimination for Algebraically Closed Fields. AISC/MKM/Calculemus Cyril Cohen, Assia Mahboubi
2010	J	`jnl`	An introduction to small scale reflection in Coq. J. Formaliz. Reason. Georges Gonthier, Assia Mahboubi
2009	—	`conf`	Packaging Mathematical Structures. TPHOLs François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
2007	—	`conf`	A Modular Formalisation of Finite Group Theory. TPHOLs Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
2007	J	`jnl`	Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. Assia Mahboubi
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	`conf`	Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. IJCAR Assia Mahboubi
2005	—	`conf`	Programming and certifying a CAD algorithm in the Coq system. Mathematics, Algorithms, Proofs Assia Mahboubi
2005	—	`conf`	Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs Benjamin Grégoire, Assia Mahboubi