2024
- titre
- Trocq: Proof Transfer for Free, With or Without Univalence
- auteur
- Cyril Cohen, Enzo Crance, Assia Mahboubi
- article
- ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268
- Accès au texte intégral et bibtex
-
- titre
- A First Order Theory of Diagram Chasing
- auteur
- Assia Mahboubi, Matthieu Piquerez
- article
- CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. pp.1-19
- Accès au texte intégral et bibtex
-
- titre
- Machine-Checked Categorical Diagrammatic Reasoning
- auteur
- Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
- article
- 2024
- Accès au texte intégral et bibtex
-
2023
- titre
- Manifest Termination
- auteur
- Assia Mahboubi, Guillaume Melquiond
- article
- TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3
- Accès au texte intégral et bibtex
-
- titre
- Compositional pre-processing for automated reasoning in dependent type theory
- auteur
- Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
- article
- CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
- Accès au texte intégral et bibtex
-
2022
- titre
- Trakt : Uniformiser les types pour automatiser les preuves (démonstration)
- auteur
- Denis Cousineau, Enzo Crance, Assia Mahboubi
- article
- JFLA 2022 - 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263
- Accès au texte intégral et bibtex
-
- titre
- Gardening with the Pythia A model of continuity in a dependent setting
- auteur
- Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
- article
- CSL 2022 - Computer Science Logic, Feb 2022, Göttingen, Germany. pp.1-19, ⟨10.4230/LIPIcs.CSL.2022.13⟩
- Accès au texte intégral et bibtex
-
2021
- titre
- Unsolvability of the Quintic Formalized in Dependent Type Theory
- auteur
- Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
- article
- ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France
- Accès au texte intégral et bibtex
-
- titre
- A formal proof of the irrationality of ζ(3)
- auteur
- Assia Mahboubi, Thomas Sibut-Pinote
- article
- Logical Methods in Computer Science, 2021, 17 (1), pp.1-25. ⟨10.23638/LMCS-17(1:16)2021⟩
- Accès au texte intégral et bibtex
-
- titre
- Machine-checked computer-aided mathematics
- auteur
- Assia Mahboubi
- article
- Logic in Computer Science [cs.LO]. Université de Nantes (UN), Nantes, FRA., 2021
- Accès au texte intégral et bibtex
-
2020
- titre
- Competing inheritance paths in dependent type theory: a case study in functional analysis
- auteur
- Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
- article
- IJCAR 2020 - International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.1-19
- Accès au texte intégral et bibtex
-
2019
- titre
- A certificate-based approach to formally verified approximations
- auteur
- Florent Bréhard, Assia Mahboubi, Damien Pous
- article
- ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.1-19, ⟨10.4230/LIPIcs.ITP.2019.8⟩
- Accès au texte intégral et bibtex
-
- titre
- Formally Verified Approximations of Definite Integrals
- auteur
- Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
- article
- Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
- Accès au texte intégral et bibtex
-
2018
- titre
- Calcul Formel et Preuves Formelles
- auteur
- Assia Mahboubi
- article
- Luminy, France. 2018, pp.1-10
- Accès au texte intégral et bibtex
-
2017
- titre
- Théories géométriques pour l'algèbre des nombres réels
- auteur
- Henri Lombardi, Assia Mahboubi
- article
- Contemporary mathematics, 2017, Ordered algebraic structures and related topics, 697, pp.239--264
- Accès au texte intégral et bibtex
-
2016
- titre
- Machine-checked mathematics
- auteur
- Assia Mahboubi
- article
- Nieuw Archief voor Wiskunde, 2016, 5/17 (3), pp.5
- Accès au texte intégral et bibtex
-
- titre
- Formally Verified Approximations of Definite Integrals
- auteur
- Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
- article
- Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩
- Accès au texte intégral et bibtex
-
- titre
- An Induction Principle over Real Numbers
- auteur
- Assia Mahboubi
- article
- Archive for Mathematical Logic, 2016, ⟨10.1007/s00153-016-0513-8⟩
- Accès au texte intégral et bibtex
-
- titre
- A Small Scale Reflection Extension for the Coq system
- auteur
- Georges Gonthier, Assia Mahboubi, Enrico Tassi
- article
- [Research Report] RR-6455, Inria Saclay Ile de France. 2016
- Accès au texte intégral et bibtex
-
2015
- titre
- Axiomatic constraint systems for proof search modulo theories
- auteur
- Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi
- article
- 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. ⟨10.1007/978-3-319-24246-0_14⟩
- Accès au bibtex
-
2014
- titre
- Computer-checked mathematics: a formal proof of the odd order theorem
- auteur
- Assia Mahboubi
- article
- 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), Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603090⟩
- Accès au bibtex
-
- titre
- Un ordinateur pour vérifier les preuves mathématiques
- auteur
- Assia Mahboubi
- article
- Images des Mathématiques, 2014
- Accès au bibtex
-
- titre
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
- auteur
- Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
- article
- ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria
- Accès au texte intégral et bibtex
-
2013
- titre
- A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ⟨10.1145/2503887.2503892⟩
- Accès au texte intégral et bibtex
-
- titre
- Canonical Structures for the working Coq user
- auteur
- Assia Mahboubi, Enrico Tassi
- article
- ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩
- Accès au texte intégral et bibtex
-
- titre
- A Machine-Checked Proof of the Odd Order Theorem
- auteur
- 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
- article
- ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
- Accès au texte intégral et bibtex
-
- titre
- The Rooster and the Butterflies
- auteur
- Assia Mahboubi
- article
- CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. pp.1-18, ⟨10.1007/978-3-642-39320-4_1⟩
- Accès au texte intégral et bibtex
-
- titre
- Homotopy Type Theory: Univalent Foundations of Mathematics
- auteur
- Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
- article
- The Univalent Foundations Program Institute for Advanced Study, pp.1--587, 2013
- Accès au bibtex
-
2012
- titre
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
- auteur
- François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
- article
- 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.67-81, ⟨10.1007/978-3-642-31365-3_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Simulating the DPLL(T ) procedure in a sequent calculus with focusing
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- 2012
- Accès au texte intégral et bibtex
-
- titre
- Two simulations about DPLL(T)
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- 2012
- Accès au texte intégral et bibtex
-
- titre
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- auteur
- Cyril Cohen, Assia Mahboubi
- article
- Logical Methods in Computer Science, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8(1:02)2012⟩
- Accès au texte intégral et bibtex
-
2011
- titre
- A formal study of Bernstein coefficients and polynomials
- auteur
- Yves Bertot, Frédérique Guilhot, Assia Mahboubi
- article
- Mathematical Structures in Computer Science, 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
- Accès au texte intégral et bibtex
-
- titre
- A Generic Formalised Framework for Reasoning About Weak Memory Models
- auteur
- Jade Alglave, Assia Mahboubi
- article
- 2011
- Accès au texte intégral et bibtex
-
2010
- titre
- A formal quantifier elimination for algebraically closed fields
- auteur
- Cyril Cohen, Assia Mahboubi
- article
- Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩
- Accès au texte intégral et bibtex
-
- titre
- An introduction to small scale reflection in Coq
- auteur
- Georges Gonthier, Assia Mahboubi
- article
- Journal of Formalized Reasoning, 2010, 3 (2), pp.95-152
- Accès au texte intégral et bibtex
-
2009
- titre
- Packaging Mathematical Structures
- auteur
- François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
- article
- Theorem Proving in Higher Order Logics, 2009, Munich, Germany
- Accès au texte intégral et bibtex
-
2007
- titre
- Implementing the cylindrical algebraic decomposition within the Coq system
- auteur
- Assia Mahboubi
- article
- Mathematical Structures in Computer Science, 2007, 17 (1), pp.99-127. ⟨10.1017/S096012950600586X⟩
- Accès au bibtex
-
- titre
- A Modular Formalisation of Finite Group Theory
- auteur
- Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
- article
- [Research Report] RR-6156, INRIA. 2007, pp.17
- Accès au texte intégral et bibtex
-
2006
- titre
- Contributions à la certification des calculs dans R : théorie, preuves, programmation
- auteur
- Assia Mahboubi
- article
- Génie logiciel [cs.SE]. Université Nice Sophia Antipolis, 2006. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Proving formally the implementation of an efficient gcd algorithm for polynomials
- auteur
- Assia Mahboubi
- article
- Automated Reasoning, Third International Joint Conference, IJCAR 2006, Aug 2006, Seattle, WA, United States. pp.438-452
- Accès au texte intégral et bibtex
-
2005
- titre
- Proving Equalities in a Commutative Ring Done Right in Coq
- auteur
- Benjamin Gregoire, Assia Mahboubi
- article
- TPHOLs 2005, Aug 2005, Oxford, United Kingdom. pp.98-113, ⟨10.1007/11541868_7⟩
- Accès au bibtex
-
- titre
- Programming and certifying a CAD algorithm in the Coq system
- auteur
- Assia Mahboubi
- article
- Dagstuhl Seminar 05021 - Mathematics, Algorithms, Proofs, Jan 2005, Dagstuhl, Germany
- Accès au bibtex
-
2002
- titre
- Élimination des quantificateurs sur les réels pour Coq
- auteur
- Assia Mahboubi, Loïc Pottier
- article
- Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France
- Accès au texte intégral et bibtex
-