Publications HAL de Assia,Mahboubi

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
https://hal.inria.fr/hal-03626851/file/jfla22_paper_9.pdf 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
https://hal.inria.fr/hal-03510671/file/gardening_with_the_pythia.pdf 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
https://hal.inria.fr/hal-03136002/file/main.pdf BibTex
titre
A formal proof of the irrationality of ζ(3)
auteur
Assia Mahboubi, Thomas Sibut-Pinote
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, 17 (1), pp.1-25. ⟨10.23638/LMCS-17(1:16)2021⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03517003/file/1912.06611.pdf 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
https://tel.archives-ouvertes.fr/tel-03107626/file/memoir_with_cover.pdf 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
https://hal.inria.fr/hal-02463336/file/ijcar%20%281%29.pdf 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
https://hal.laas.fr/hal-02088529/file/chebapprox.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex

2017

titre
Théories géométriques pour l'algèbre des nombres réels
auteur
Henri Lombardi, Assia Mahboubi
article
Contemporary mathematics, American Mathematical Society, 2017, Ordered algebraic structures and related topics, 697, pp.239--264
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426164/file/Reels-geom-court.pdf BibTex

2016

titre
Machine-checked mathematics
auteur
Assia Mahboubi
article
Nieuw Archief voor Wiskunde, Koninklijk Wiskundig Genootschap, 2016, 5/17 (3), pp.5
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01363284/file/naw5-2016-17-3-172.pdf 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
https://hal.inria.fr/hal-01289616/file/main.pdf BibTex
titre
An Induction Principle over Real Numbers
auteur
Assia Mahboubi
article
Archive for Mathematical Logic, Springer Verlag, 2016, ⟨10.1007/s00153-016-0513-8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01376054/file/main.pdf 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
https://hal.inria.fr/inria-00258384/file/main.pdf 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
https://arxiv.org/pdf/1412.6790 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
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
https://hal.inria.fr/hal-00984057/file/main.pdf BibTex
titre
Un ordinateur pour vérifier les preuves mathématiques
auteur
Assia Mahboubi
article
Images des Mathématiques, CNRS, 2014
Accès au bibtex
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
https://hal.inria.fr/hal-00854426/file/DPLL-LK.pdf 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
https://hal.inria.fr/hal-00816703/file/main.pdf 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
https://hal.inria.fr/hal-00816699/file/main.pdf 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
https://hal.inria.fr/hal-00825074/file/main.pdf 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
Aucun, pp.448, 2013
Accès au bibtex
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
https://hal.inria.fr/hal-00687640/file/main.pdf 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
https://hal.inria.fr/hal-00690392/file/MainHal.pdf 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
https://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf 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, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8(1:02)2012⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593738/file/1201.3731.pdf 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, Cambridge University Press (CUP), 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503017/file/check_version_Jan_2011.pdf 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
https://hal.inria.fr/inria-00604656/file/itp.pdf 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
https://hal.inria.fr/inria-00464237/file/main.pdf BibTex
titre
An introduction to small scale reflection in Coq
auteur
Georges Gonthier, Assia Mahboubi
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2010, 3 (2), pp.95-152
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00515548/file/main-rr.pdf 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
https://hal.inria.fr/inria-00368403/file/main.pdf BibTex

2007

titre
Implementing the cylindrical algebraic decomposition within the Coq system
auteur
Assia Mahboubi
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2007, 17 (1), pp.99-127. ⟨10.1017/S096012950600586X⟩
Accès au bibtex
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
https://hal.inria.fr/inria-00139131/file/RR-6156.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00117409/file/these_assia_mahboubi.pdf 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
https://hal.inria.fr/inria-00001270/file/SousRes.pdf 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
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
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
https://hal.inria.fr/hal-00819482/file/jfla02.pdf BibTex