Amina Doumane
Cet article est une ébauche concernant une personnalité marocaine et l’informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
| Naissance | |
|---|---|
| Nationalité | |
| Formation | |
| Activités |
| Directeur de thèse |
Pierre-Louis Curien (d) |
|---|---|
| Site web | |
| Distinctions |
Prix Gilles-Kahn () Prix Kleene (en) () |
Amina Doumane (en arabe : أمينة دومان), née le , est une informaticienne théoricienne marocaine, pionnière[1] pour avoir prouvé un théorème important de logique mathématique, le théorème de complétude pour le μ-calcul linéaire, et ce de manière constructive (i.e. en produisant un certificat). Par ce travail, elle fait le pont entre logique mathématique et vérification des propriétés infinitaires des logiciels, ce qui permet de raisonner à la fois de manière inductive et coinductive.
Sa thèse permet de montrer que les preuves circulaires ont un réel statut de preuve théorique et qu'elles peuvent être appliquées à d’autres domaines comme la vérification formelle.
Biographie[modifier | modifier le code]
Amina Doumane est née le [2] au Maroc[3].
Elle suit ses études secondaires au lycée Chourouk de Khouribga où elle obtient en 2008 le baccalauréat scientifique avec mention très bien. Elle représente le Maroc aux Olympiades internationales de mathématiques puis elle entre en classes préparatoires au lycée Ibn Abdoun de Khouribga avant d'entrer en MP* au lycée Moulay Youssef de Rabat.
Elle intègre en 2010 l'École Centrale Paris, en spécialité mathématiques appliquées.
En 2014, Amina Doumane bénéficie d'une bourse de la région Ile-de-France dans le cadre du domaine d'intérêt majeur « Recherche doctorale en mathématiques-IDF », rebaptisé depuis « DIM Math Innov »[3].
De 2014 à 2017, elle prépare sa thèse de Doctorat intitulée On the infinitary proof theory of logics with fixed points (Sur la théorie de la démonstration infinitaire pour les logiques à points fixes)[4], dirigée par David Baelde, Pierre-Louis Curien et Alexis Saurin à l'Université Paris Diderot.
Elle travaille depuis comme chercheure postdoctorale à l'Université de Varsovie avec Mikołaj Bojańczyk et au Laboratoire d’informatique du parallélisme (LIP) de l'ENS Lyon avec Damien Pous.
Travaux[modifier | modifier le code]
Les travaux d'Amina Doumane s'inscrivent dans le cadre de la théorie de la démonstration[1].
Utilisées entre autres pour la vérification de programmes informatiques, les logiques infinitaires permettent des formules ou des démonstrations infiniment longues.
Le résultat obtenu concerne le « théorème de complétude ». Ce dernier dit que si une formule est vraie, alors elle est prouvable. L'Américain Dexter Kozen en 1983 puis Roope Kaivola[5] en 1995 avaient apporté une démonstration de ce théorème dans le cadre du µ-calcul[a], mais de manière non constructive, à savoir que l'on savait que la preuve existe mais on n'était pas en mesure de produire cette preuve.
Le travail d'Amina Doumane permet désormais de certifier qu'un système informatique répond bien aux exigences qui lui sont spécifiées, tout en produisant le certificat qui le prouve. « Le certificat est une expression mathématique, preuve de cette implication, que l'on peut communiquer à d'autres personnes qui, en plus, sauront pourquoi le système satisfait la propriété : le certificat a une vertu explicative » selon les mots de la chercheure.
Pour y parvenir, Amina Doumane a réussi à concevoir un algorithme qui permet à partir d'une formule de µ-calcul de construire automatiquement une preuve[6]. Cette formule de µ-calcul peut être la « grande implication » exprimant que le système (S) vérifie la propriété (P), à savoir que (S) ⇒ (P) est vrai. Pour obtenir la preuve constructive, elle décompose toute formule de µ-calcul en sous-formules intermédiaires, puis elle prouve chacune grâce à des preuves infinitaires. Enfin elle applique à chacune de ces preuves un algorithme qu'elle a mis au point permettant de transformer une preuve infinitaire en preuve usuelle[1]. La difficulté réside dans le choix des décompositions. Pour y parvenir, elle s'est inspirée de la théorie des automates qui offre des outils pour surmonter les difficultés que sont l'alternance (de ∧ et ∨), les conditions de parité (alternance de μ et ν) et le non-déterminisme (présence de ∨)[7].
Publications[modifier | modifier le code]
- On the infinitary proof theory of logics with fixed points, 2017, thèse soutenue à l’Université Paris Diderot (Paris 7) Sorbonne Paris Cité et préparée à l’Institut de Recherche en Informatique Fondamentale (IRIF) et au Laboratoire spécification et vérification (LSV) sous la direction de David Baelde, Alexis Saurin et Pierre-Louis Curien.
- Constructive completeness for the linear-time μ-calculus, 2017 DOI:10.1109/LICS.2017.8005075.
Récompenses[modifier | modifier le code]
- 2017 : Prix Gilles-Kahn[8] ;
- 2017 : Prix Kleene ;
- 2018 : Prix La Recherche[1],[9].
Notes et références[modifier | modifier le code]
Notes[modifier | modifier le code]
- R. Kaivola démontre le théorème de complétude du μ-calcul : « Si une formule du μ-calcul est valide, alors elle est prouvable dans le système de Kozen ».
Références[modifier | modifier le code]
- Prix La Recherche 2018 : Prouver à l'aide de l'infini
- « CV d'Amina Doumane », sur ens-lyon.fr (consulté le )
- « Aide à la recherche : Amina Doumane décroche le prix Gilles-Kahn », sur www.iledefrance.fr, (consulté le )
- « Amina Doumane, On the infinitary proof theory of logics with fixed points », (consulté le )
- Roope Kaivola, Axiomatising Linear Time Mu-calculus, 1995.
- « Prix de thèse Gilles Kahn et Prix La Recherche pour Amina Doumane » (consulté le )
- Support visuel de la soutenance de thèse.
- « Prix de thèse - Lauréats 2017 » (consulté le )
- Prix La Recherche 2018 - Palmarès
Liens externes[modifier | modifier le code]
- (en) Site officiel
- Ressources relatives à la recherche :
- Exposé de soutenance de thèse : visuel & présentation orale.
