×
Author ID: mahboubi.assia Recent zbMATH articles by "Mahboubi, Assia"
Published as: Mahboubi, Assia
Homepage: https://specfun.inria.fr/mahboubi/
External Links: MGP · dblp
all top 5

Co-Authors

5 single-authored
6 Cohen, Cyril
5 Gonthier, Georges
4 Avigad, Jeremy
4 Sibut-Pinote, Thomas
4 Tassi, Enrico
3 Bertot, Yves
3 Melquiond, Guillaume
3 Rideau, Laurence
2 Bezem, Marc
2 Garillot, François
2 Lombardi, Henri
2 Rouhling, Damien
2 Théry, Laurent
1 Aczel, Peter
1 Affeldt, Reynald
1 Ahrens, Benedikt
1 Altenkirch, Thorsten
1 Angiuli, Carlo
1 Asperti, Andrea
1 Awodey, Steve
1 Barras, Bruno
1 Bauer, Andrej
1 Bernard, Sophie
1 Bobot, François
1 Bordg, Anthony
1 Bréhard, Florent
1 Brunerie, Guillaume
1 Chyzak, Frédéric
1 Conchon, Sylvain
1 Constable, Robert Lee
1 Contejean, Evelyne
1 Coquand, Thierry
1 Curien, Pierre-Louis
1 Dybjer, Peter
1 Farooque, Mahfuza
1 Finster, Eric
1 Gambino, Nicola
1 Garner, Richard
1 Graham-Lengrand, Stéphane
1 Grayson, Daniel Richard
1 Grégoire, Benjamin
1 Guilhot, Frédérique
1 Hales, Thomas Callister
1 Harper, Robert
1 Herbelin, Hugo
1 Hofmann, Martin
1 Hofstra, Pieter J. W.
1 Hötzel Escardó, Martín
1 Hou (Favonia), Kuen-Bang
1 Iguernelala, Mohamed
1 Joyal, André
1 Kapulkin, Krzysztof
1 Kerjean, Marie
1 Kock, Joachim
1 Kraus, Nicolai
1 Leroux, Stéphane
1 Li, Nuo
1 Licata, Dan
1 Lumsdaine, Peter LeFanu
1 Luo, Zhaohui
1 Martin-Löf, Per
1 Mebsout, Alain
1 Melikhov, Sergey Aleksandrovich
1 Nahas, Michael
1 Notin, Jean-Marc
1 O’Connor, Russell
1 Ould Biha, Sidi
1 Palmgren, Erik
1 Paşca, Ioana
1 Pelayo, Alvaro
1 Polonsky, Andrew
1 Pous, Damien
1 Riehl, Emily
1 Rijke, Egbert
1 Sakaguchi, Kazuhiko
1 Scott, Dana Stewart
1 Scott, Philip J.
1 Shulman, Michael A.
1 Sojakova, Kristina
1 Solov’ëv, Sergeĭ Vladimirovich
1 Solovyev, Alexey
1 Sozeau, Matthieu
1 Spitters, Bas
1 Strub, Pierre-Yves
1
1 Van den Berg, Benno
1 Voevodskiĭ, Vladimir Aleksandrovich
1 Warren, Michael Alton
1 Zeilberger, Noam

Publications by Year

Citations contained in zbMATH Open

21 Publications have been cited 239 times in 175 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
59
2013
An introduction to small scale reflection in Coq. Zbl 1211.68368
Gonthier, Georges; Mahboubi, Assia
36
2010
Packaging mathematical structures. Zbl 1252.68253
Garillot, François; Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence
28
2009
A modular formalisation of finite group theory. Zbl 1144.68356
Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence; Tassi, Enrico; Théry, Laurent
21
2007
Canonical structures for the working Coq user. Zbl 1317.68221
Mahboubi, Assia; Tassi, Enrico
17
2013
Proving equalities in a commutative ring done right in Coq. Zbl 1152.68702
Grégoire, Benjamin; Mahboubi, Assia
16
2005
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096
Cohen, Cyril; Mahboubi, Assia
15
2012
Implementing the cylindrical algebraic decomposition within the Coq system. Zbl 1121.03023
Mahboubi, Assia
9
2007
A computer-algebra-based formal proof of the irrationality of \(\zeta (3)\). Zbl 1416.68155
Chyzak, Frédéric; Mahboubi, Assia; Sibut-Pinote, Thomas; Tassi, Enrico
9
2014
A formal study of Bernstein coefficients and polynomials. Zbl 1236.33016
Bertot, Yves; Guilhot, Frédérique; Mahboubi, Assia
5
2011
Formally verified approximations of definite integrals. Zbl 1468.68300
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas
4
2016
Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659
Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko
4
2020
Formally verified approximations of definite integrals. Zbl 1468.68301
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas
3
2019
Proving formally the implementation of an efficient gcd algorithm for polynomials. Zbl 1222.68369
Mahboubi, Assia
3
2006
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. Zbl 1358.68249
Bobot, François; Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed; Mahboubi, Assia; Mebsout, Alain; Melquiond, Guillaume
3
2012
A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394
Cohen, Cyril; Mahboubi, Assia
2
2010
A certificate-based approach to formally verified approximations. Zbl 07649957
Bréhard, Florent; Mahboubi, Assia; Pous, Damien
2
2019
A formal proof of the irrationality of \(\zeta(3)\). Zbl 1509.68311
Mahboubi, Assia; Sibut-Pinote, Thomas
1
2021
Geometric theories for the algebra of real numbers. (Théories géométriques pour l’algèbre des nombres réels.) Zbl 1393.13048
Lombardi, Henri; Mahboubi, Assia
1
2017
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. Zbl 1391.68001
1
2018
A formal proof of the irrationality of \(\zeta(3)\). Zbl 1509.68311
Mahboubi, Assia; Sibut-Pinote, Thomas
1
2021
Competing inheritance paths in dependent type theory: a case study in functional analysis. Zbl 07614659
Affeldt, Reynald; Cohen, Cyril; Kerjean, Marie; Mahboubi, Assia; Rouhling, Damien; Sakaguchi, Kazuhiko
4
2020
Formally verified approximations of definite integrals. Zbl 1468.68301
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas
3
2019
A certificate-based approach to formally verified approximations. Zbl 07649957
Bréhard, Florent; Mahboubi, Assia; Pous, Damien
2
2019
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. Zbl 1391.68001
1
2018
Geometric theories for the algebra of real numbers. (Théories géométriques pour l’algèbre des nombres réels.) Zbl 1393.13048
Lombardi, Henri; Mahboubi, Assia
1
2017
Formally verified approximations of definite integrals. Zbl 1468.68300
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas
4
2016
A computer-algebra-based formal proof of the irrationality of \(\zeta (3)\). Zbl 1416.68155
Chyzak, Frédéric; Mahboubi, Assia; Sibut-Pinote, Thomas; Tassi, Enrico
9
2014
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
59
2013
Canonical structures for the working Coq user. Zbl 1317.68221
Mahboubi, Assia; Tassi, Enrico
17
2013
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Zbl 1241.68096
Cohen, Cyril; Mahboubi, Assia
15
2012
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. Zbl 1358.68249
Bobot, François; Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed; Mahboubi, Assia; Mebsout, Alain; Melquiond, Guillaume
3
2012
A formal study of Bernstein coefficients and polynomials. Zbl 1236.33016
Bertot, Yves; Guilhot, Frédérique; Mahboubi, Assia
5
2011
An introduction to small scale reflection in Coq. Zbl 1211.68368
Gonthier, Georges; Mahboubi, Assia
36
2010
A formal quantifier elimination for algebraically closed fields. Zbl 1286.68394
Cohen, Cyril; Mahboubi, Assia
2
2010
Packaging mathematical structures. Zbl 1252.68253
Garillot, François; Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence
28
2009
A modular formalisation of finite group theory. Zbl 1144.68356
Gonthier, Georges; Mahboubi, Assia; Rideau, Laurence; Tassi, Enrico; Théry, Laurent
21
2007
Implementing the cylindrical algebraic decomposition within the Coq system. Zbl 1121.03023
Mahboubi, Assia
9
2007
Proving formally the implementation of an efficient gcd algorithm for polynomials. Zbl 1222.68369
Mahboubi, Assia
3
2006
Proving equalities in a commutative ring done right in Coq. Zbl 1152.68702
Grégoire, Benjamin; Mahboubi, Assia
16
2005
all top 5

Cited by 314 Authors

8 Paulson, Lawrence Charles
7 Affeldt, Reynald
6 Cohen, Cyril
6 Mahboubi, Assia
5 Heras, Jónathan
5 Kaliszyk, Cezary
5 Narboux, Julien
5 Rabe, Florian
4 Asperti, Andrea
4 Doczkal, Christian
4 Smolka, Gert
4 Théry, Laurent
3 Allamigeon, Xavier
3 Aransay, Jesús
3 Avigad, Jeremy
3 Bertot, Yves
3 Coquand, Thierry
3 Gonthier, Georges
3 Kohlhase, Michael
3 Li, Wenda
3 Melquiond, Guillaume
3 Nowak, David E.
3 Rouhling, Damien
3 Rubio García, Julio Jesús
3 Tassi, Enrico
3 Zhan, Bohua
2 Ahrens, Benedikt
2 Akbarpour, Behzad
2 Baanen, Anne
2 Ballarin, Clemens
2 Birkedal, Lars
2 Boulmé, Sylvain
2 Boutry, Pierre
2 Braibant, Thomas
2 Bréhard, Florent
2 Bromberger, Martin
2 Carette, Jacques
2 Chan, Hing-Lun
2 Dagand, Pierre-Evariste
2 Davenport, James Harold
2 Dénès, Maxime
2 Domínguez, César
2 Dreyer, Derek R.
2 Dufourd, Jean-François
2 Dumbrava, Stefania
2 England, Matthew
2 Farmer, William M.
2 Garrigue, Jacques
2 Kapulkin, Krzysztof
2 Katz, Ricardo David
2 Komendantskaya, Ekaterina
2 Komendantsky, Vladimir
2 Konovalov, Olexandr
2 Krebbers, Robbert
2 Linton, Stephen A.
2 Magron, Victor
2 Maréchal, Alexandre
2 Muñoz, César A.
2 Nanevski, Aleksandar
2 Narkawicz, Anthony Joseph
2 Nipkow, Tobias
2 Norrish, Michael
2 O’Connor, Russell
2 Ould Biha, Sidi
2 Paşca, Ioana
2 Pous, Damien
2 Poza, María
2 Ricciotti, Wilmer
2 Rideau, Laurence
2 Sacerdoti Coen, Claudio
2 Saikawa, Takafumi
2 Sakaguchi, Kazuhiko
2 Schreck, Pascal
2 Sibut-Pinote, Thomas
2 Spitters, Bas
2 Stojanović Đurđević, Sana
2 Strub, Pierre-Yves
2 Tabareau, Nicolas
2 Thiemann, René
2 Urban, Josef
2 Weidenbach, Christoph
2 Wenzel, Makarius
2 Yamada, Akihisa
1 Abbott, John A.
1 Ábrahám, Erika
1 Adams, Mark
1 Adams, Robin
1 Anand, Abhishek
1 Armstrong, Alasdair
1 Avelar, Andréia Borges
1 Awodey, Steve
1 Ayala-Rincón, Mauricio
1 Bancerek, Grzegorz
1 Barbosa, Haniel
1 Barrett, Clark W.
1 Bauer, Gertrud
1 Becker, Bernd
1 Benzaken, Véronique
1 Bernard, Sophie
1 Besson, Frédéric
...and 214 more Authors

Citations by Year