Home
Olivier Nicole
Hello, I’m Olivier. During daytime, I work for Tarides on the OCaml language, which is a high-level language, both safe and performant, that I like a lot. I generally work on free or open source software, so you can consult my current activity on my Github profile.
Part of the rest of my time is spent reading philosophy or various novels (with an inclination toward SF), or hacking on a typesetting software.
Before my current job, I did a PhD at CEA List and ENS under the supervision of Matthieu Lemerre and Xavier Rival. I worked on static analysis of low-level code in order to verify the security of OS kernels (among other things).
I'm also interested in functional programming, type systems and logic.
My name is pronounced ɔ.li'vje ni'kol, but “Oliver” with the usual English pronunciation is also fine.
Personal projects
- I have contributed to implement mathematics typesetting into the SILE typesetter.
- haskell-chess: a ridiculously simple and incomplete chess engine in Haskell. May be completed some day.
- spino: an attempt to encode the logical structure of Spinoza’s “Ethics” in the proof language Agda. The work is based on Jarrett, The logical structure of Spinoza's Ethics, Part I.
Communications
- Runtime Detection of Data Races in OCaml with ThreadSanitizer (extended abstract) (slides) (video, sorry about the terrible sound)
Olivier Nicole and Fabrice Buoro
OCaml Workshop 2023 - Multicoretests – Parallel Testing Libraries for OCaml 5.0 (extended abstract) (video)
Jan Midtgaard, Olivier Nicole and Nicolas Osborne
OCaml Workshop 2022 -
Automatically Proving Microkernel Security
(slides,
video in French)
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/Demo Talk) (pdf)
Olivier Nicole, Leo White and Jeremy Yallop
PEPM 2018
Publications
-
MacoCaml: Staging Composable and Compilable Macros
(paper)
Ningning Xie, Leo White, Olivier Nicole and 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)
(artifact)
(presentation video)
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
RTAS 2021 (IEEE Real-Time and Embedded Technology and Applications Symposium)
Best Paper Award
PhD thesis
Automated Verification of Systems Code using Type-based Memory Abstractions
- PDF for screens, for printing (hyperlinks not colored)
- Video of the defense (in English)
Teaching
2020–2021
- Mathematics S1: Elementary logic. L1 level, CRI Paris (12 h)
- Mathematics S2: Linear algebra. L1 level, CRI Paris (12 h)
2019–2020
- Éléments de programmation (Elements of Programming) — LU1IN001. L1 level, Sorbonne Université (19 h)
- Programmation en C (C Programming) — PRC05. L3 level, École d'ingénieurs Denis Diderot, Université Paris 7 (27 h)
2018–2019
- Systèmes d'exploitations (Operating Systems) — IN201. M1 level, ENSTA Paris (15 h)
