Accueil
Olivier Nicole
Salut, moi c’est Olivier et en journée, je travaille à l’Inria sur le langage OCaml, qui est un langage haut niveau à la fois sûr et performant que j'apprécie beaucoup. Je travaille en général sur des logiciels libres ou open source, donc ce que je fais en ce moment peut être consulté sur mon profil Github.
Le reste du temps, je lis de la philo ou divers romans (avec un penchant pour la SF), ou bien des livres de vulgarisation scientifique (j’adore ceux de Carlo Rovelli). J’aime aussi apprendre des choses sur l’histoire : l’histoire des sciences, de la politique, du monde… et sur la société. Pourquoi les humains agissent-ils de la manière dont ils agissent ?
Avant mon emploi actuel, j'ai préparé et soutenu un doctorat au CEA List et à l’ENS sous la supervision de Matthieu Lemerre et Xavier Rival. Il porte sur l'analyse statique de code bas niveau afin de vérifier la sécurité de noyaux de systèmes d’exploitation (notamment). Après cette thèse, j’ai travaillé à Tarides pendant 4 ans sur le langage OCaml et son écosystème.
Outre l'analyse statique, je m’intéresse aussi à la programmation fonctionnelle en général, aux systèmes de types et aux systèmes logiques.
Projets personnels
- J’ai contribué à implémenter le rendu des mathématiques dans le logiciel typographique SILE.
- haskell-chess: un moteur d’échecs ridiculement simple, et incomplet. Sera peut-être terminé un jour.
- spino: une tentative (incomplète) d’encoder la structure logique de L’Éthique de Spinoza dans le langage de preuve Agda. Le travail se base sur Jarrett, The logical structure of Spinoza's Ethics, Part I.
Communications
- Runtime Detection of Data Races in OCaml with ThreadSanitizer (résumé long) (diapos) (vidéo, désolé pour la mauvaise qualité du son)
Olivier Nicole et Fabrice Buoro
OCaml Workshop 2023 - Multicoretests – Parallel Testing Libraries for OCaml 5.0 (résumé long)
Jan Midtgaard, Olivier Nicole et Nicolas Osborne
OCaml Workshop 2022 -
Automatically Proving Microkernel Security
(diapos,
vidéo)
Olivier Nicole
RESSI 2020 (Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information), short paper - Modular Macros (Poster/Démonstration) (pdf)
Olivier Nicole, Leo White et Jeremy Yallop
PEPM 2018
Publications
-
MacoCaml: Staging Composable and Compilable Macros
(article)
Ningning Xie, Leo White, Olivier Nicole et Jeremy Yallop
ICFP 2023 (International Conference on Functional Programming) -
Lightweight Shape Analysis based on Physical Types
(pre-print)
Olivier Nicole, Matthieu Lemerre, Xavier Rival
VMCAI 2022 (Verification, Model Checking and Abstract Interpretation) -
No Crash, No Exploit: Automated Verification of Embedded Kernels
(pre-print)
(artefact)
(vidéo de la présentation)
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
RTAS 2021 (IEEE Real-Time and Embedded Technology and Applications Symposium)
Best Paper Award
Thèse
Vérification automatisée de code système à l’aide d’abstractions mémoire basées sur le typage
- PDF pour lecture sur écran, pour impression (hyperliens non colorés)
- Soutenance (en anglais)
Enseignement
2020–2021
- Mathématiques S1: Bases de la logique. L1, CRI Paris (12 h)
- Mathématiques S2: Algèbre linéaire. L1, CRI Paris (12 h)
2019–2020
- Éléments de programmation — LU1IN001. L1, Sorbonne (19 h)
- Programmation en C — PRC05. L3, École d’ingénieurs Paris Diderot, Université Paris 7 (27 h)
2018–2019
- Systèmes d’exploitation — IN201. M1, ENSTA Paris (15 h)
