MSR-INRIAResearcher - Assia Mahboubi - Microsoft Research Inria Joint Centre

2016

Reports

2015

Conference papers

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

Journal articles

Conference papers

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: 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

Conference papers

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

Books

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

2012

Journal articles

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

Conference papers

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

Reports

2011

Preprints, Working Papers, …

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

Journal articles

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

Conference papers

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

2009

Conference papers

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

Reports

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

Researchers