I am a tenured researcher (directrice de recherche)
at Inria, in
the Gallinette team, Nantes, France.
I am also an endowed professor in the
and Number Theory section of the
Vrije Universiteit Amsterdam, in the Netherlands.
My research interests revolve around the foundations and formalization
of mathematics in type theory and the automated verification of
mathematical proofs. In particular, I am interested in the new
insights that one often gets on familiar mathematical objects when
looking for their most adequate formal representation for the purpose
of computer-aided proof checking. I also have a special interest for
the interplay between computer algebra and formal proofs, and more
generally for computer-aided mathematics. I am a
happy, intensive user of the Coq
interactive proof assistant, and a lead developer of the
Mathematical Components libraries.
Beyond the Lab ⋅
- I will give an invited talk at the Workshop in Honour of Thierry Coquand's 60th Birthday.
- I have obtained an ERC Consolidator grant for the FRESCO (Fast and Reliable Symbolic Computation) project. The project has started November 1st 2021.
- Enzo Crance
(PhD candidate, automation for interactive theorem provers,
co-supervisor: Denis Cousineau)
- Martin Baillon (PhD candidate, syntactic models of type theory and continuity principles, co-supervisor: Pierre-Marie Pédrot)
- Chris Hughes (PhD candidate, Transport of mathematical properties in type theory, co-supervisor: Cyril Cohen)
My publications are listed and archived
on HAL. My
DBLP page is here.
is the web page of the course "Machine-Checked Mathematics" at the
Vrije Universiteit Amsterdam.
- I taught an introductory course to Coq at the Coq Andes Summer School, in San José del Maipo, Chile.
- Mathématiques assistées par ordinateur, Collège de France, 2018.
Beyond the Lab
UFR Sciences et Techniques
2, rue de la Houssinière
44322 Nantes Cedex 3
Email: Assia.Mahboubi [at] inria.fr