Mathematical Components

• Boris Djalal Microsoft Research – Inria Joint Centre

• Andrea Asperti University of Bologna (Visiting Professor)
• Jeremy Avigad Carnegie Mellon University (Invited)
• Bruno Barras Inria Saclay – Île-de-France
• Yves Bertot INRIA Sophia Antipolis – Méditerranée
• Guillaume Cano Inria Sophia Antipolis – Méditerranée
• Cyril Cohen PhD student
• Maxime Dénès Inria Sophia Antipolis – Méditerranée
• François Garillot Microsoft Research- Inria (PhD Student)
• Georges Gonthier MSR Cambridge
• Nicolas Julien PhD Student
• Stéphane Le Roux Microsoft Research-Inria (Post Doctoral Student)
• Assia Mahboubi Inria Saclay Ile de France
• Sean McLaughlin Microsoft Research-Inria (PhD Student)
• Guillaume Melquiond Microsoft Research – Inria Joint Centre (Post Doc)
• Russell O’Connor McMaster University ( Inviteed researcher)
• Sidi Ould Biha Microsoft Research-Inria (PhD Student)
• Ioana Pasca Microsoft Research-Inria (PHD Student)
• Laurence Rideau
• Alexey Solovyev Microsoft Research-Inria (Internship)
• Enrico Tassi INRIA Saclay – Île-de-France
• Laurent Théry Inria Sophia Antipolis – Méditerranée
• Benjamin Werner (Arithmetic leader), École Polytechnique
• Noam Zeilberger Microsoft Research-Inria Joint Centre
• Roland Zumkeller Microsoft Reasearch-Inria (Post Doc)

2019

Communication dans un congrès

titre

Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

auteur

Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry

article

ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 – 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-02303987/file/LIPIcs-ITP-2019-13.pdfhttps://hal.inria.fr/hal-02303987/file/LIPIcs-ITP-2019-13.pdf BibTexBibTex

2016

Rapport

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.pdfhttps://hal.inria.fr/inria-00258384/file/main.pdf BibTexBibTex

2015

Communication dans un congrès

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.6790https://arxiv.org/pdf/1412.6790 BibTexBibTex

2014

Article dans une revue

titre

Un ordinateur pour vérifier les preuves mathématiques

auteur

Assia Mahboubi

article

Images des Mathématiques, CNRS, 2014

Accès au bibtex

BibTexBibTex

Communication dans un congrès

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.pdfhttps://hal.inria.fr/hal-00984057/file/main.pdf BibTexBibTex

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

BibTexBibTex

Rapport

titre

Coq 8.4 Reference Manual

auteur

Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi

article

[Research Report] Inria. 2014

Accès au bibtex

BibTexBibTex

2013

Communication dans un congrès

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.pdfhttps://hal.inria.fr/hal-00816703/file/main.pdf BibTexBibTex

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.pdfhttps://hal.inria.fr/hal-00825074/file/main.pdf BibTexBibTex

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.pdfhttps://hal.inria.fr/hal-00816699/file/main.pdf BibTexBibTex

titre

Refinements for Free!

auteur

Cyril Cohen, Maxime Dénès, Anders Mörtberg

article

Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 – 162, ⟨10.1007/978-3-319-03545-1_10⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-01113453/file/refinements.pdfhttps://hal.inria.fr/hal-01113453/file/refinements.pdf BibTexBibTex

Ouvrage (y compris édition critique et traduction)

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

BibTexBibTex

2012

Article dans une revue

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.pdfhttps://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTexBibTex

Communication dans un congrès

titre

Construction of real algebraic numbers in Coq

auteur

Cyril Cohen

article

ITP – 3rd International Conference on Interactive Theorem Proving – 2012, Aug 2012, Princeton, United States

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-00671809/file/main.pdfhttps://hal.inria.fr/hal-00671809/file/main.pdf BibTexBibTex

titre

A language of patterns for subterm selection

auteur

Georges Gonthier, Enrico Tassi

article

ITP, Aug 2012, Princeton, United States. pp.361-376, ⟨10.1007/978-3-642-32347-8_25⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-00652286/file/rew.pdfhttps://hal.inria.fr/hal-00652286/file/rew.pdf BibTexBibTex

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.pdfhttps://hal.inria.fr/hal-00687640/file/main.pdf BibTexBibTex

titre

Construction des nombres algébriques réels en Coq

auteur

Cyril Cohen

article

JFLA – Journées Francophones des Langages Applicatifs – 2012, Feb 2012, Carnac, France

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-00665965/file/paper_11.pdfhttps://hal.inria.fr/hal-00665965/file/paper_11.pdf BibTexBibTex

Rapport

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.pdfhttps://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf BibTexBibTex

Thèse

titre

Formalized algebraic numbers: construction and first-order theory.

auteur

Cyril Cohen

article

Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English

Accès au texte intégral et bibtex

https://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdfhttps://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf BibTexBibTex

2011

Communication dans un congrès

titre

Point-Free, Set-Free Concrete Linear Algebra

auteur

Georges Gonthier

article

Interactive Theorem Proving – ITP 2011, Radboud University of Nijmegen, Aug 2011, Berg en Dal, Netherlands. pp.103-118, ⟨10.1007/978-3-642-22863-6_10⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-00805966/file/main.pdfhttps://hal.inria.fr/hal-00805966/file/main.pdf BibTexBibTex

titre

CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory

auteur

Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang

article

Twenty-Sixth Annual IEEE Symposium on “Logic in Computer Science” – LICS 2011, Jun 2011, Toronto, Canada

Accès au texte intégral et bibtex

https://hal.inria.fr/inria-00583136/file/coq-mtu-lics-2011.pdfhttps://hal.inria.fr/inria-00583136/file/coq-mtu-lics-2011.pdf BibTexBibTex

Thèse

titre

Generic Proof Tools and Finite Group Theory

auteur

François Garillot

article

Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2011. English

Accès au texte intégral et bibtex

https://pastel.archives-ouvertes.fr/pastel-00649586/file/manuscript.pdfhttps://pastel.archives-ouvertes.fr/pastel-00649586/file/manuscript.pdf BibTexBibTex

Pré-publication, Document de travail

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.pdfhttps://hal.inria.fr/inria-00604656/file/itp.pdf BibTexBibTex

2010

Article dans une revue

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.pdfhttps://hal.inria.fr/inria-00515548/file/main-rr.pdf BibTexBibTex

Communication dans un congrès

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.pdfhttps://hal.inria.fr/inria-00464237/file/main.pdf BibTexBibTex

Pré-publication, Document de travail

titre

Formalizing real analysis for polynomials

auteur

Cyril Cohen

article

2010

Accès au texte intégral et bibtex

https://hal.inria.fr/inria-00545778/file/main.pdfhttps://hal.inria.fr/inria-00545778/file/main.pdf BibTexBibTex

2009

Article dans une revue

titre

Computing predecessor and successor in rounding to nearest

auteur

Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond

article

BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/inria-00337537/file/RuZiBoMe08.pdfhttps://hal.inria.fr/inria-00337537/file/RuZiBoMe08.pdf BibTexBibTex

Communication dans un congrès

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.pdfhttps://hal.inria.fr/inria-00368403/file/main.pdf BibTexBibTex

Rapport

titre

An Ssreflect Tutorial

auteur

Georges Gonthier, Roux Stéphane Le

article

[Technical Report] RT-0367, INRIA. 2009, pp.33

Accès au texte intégral et bibtex

https://hal.inria.fr/inria-00407778/file/RT-367.pdfhttps://hal.inria.fr/inria-00407778/file/RT-367.pdf BibTexBibTex

2008

Communication dans un congrès

titre

Floating-point arithmetic in the Coq system

auteur

Guillaume Melquiond

article

8th Conference on Real Numbers and Computers, Jul 2008, Santiago de Compostela, Spain. pp.93-102

Accès au texte intégral et bibtex

https://hal.inria.fr/hal-01780385/file/08-rnc8-article.pdfhttps://hal.inria.fr/hal-01780385/file/08-rnc8-article.pdf BibTexBibTex

titre

Proving bounds on real-valued functions with computations

auteur

Guillaume Melquiond

article

International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. pp.2-17, ⟨10.1007/978-3-540-71070-7_2⟩

Accès au texte intégral et bibtex

https://hal.archives-ouvertes.fr/hal-00180138/file/article.pdfhttps://hal.archives-ouvertes.fr/hal-00180138/file/article.pdf BibTexBibTex

titre

Canonical Big Operators

auteur

Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca

article

Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. ⟨10.1007/978-3-540-71067-7⟩

Accès au texte intégral et bibtex

https://hal.inria.fr/inria-00331193/file/main.pdfhttps://hal.inria.fr/inria-00331193/file/main.pdf BibTexBibTex

2007

Rapport

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.pdfhttps://hal.inria.fr/inria-00139131/file/RR-6156.pdf BibTexBibTex