Hejmo
Olivier Nicole
Saluton, mi nomiĝas Olivier. Tagtempe, mi laboras en Inria sur la programlingvo OCaml, kiu estas altnivela lingvo, samtempe sekura kaj malmultekosta je resursoj, kiu mi tre ŝatas. Mi kutime laboras sur liberaj aŭ malfermitkodaj programaroj, do miaj nunaj aferoj videblas en mia Github-profilo.
Cetertempe, mi legas filozofion aŭ diversaj romanoj (kun ŝatado por la SF) aŭ scienca disvastigado (mi tre ŝatas la librojn de Carlo Rovelli). Ankaŭ plaĉas al mi legi pri historio: historio de la sciencoj, de politiko, de la mundo… Kial la homoj agas tiel, kiel ili agas?
Antaŭ mia nuna laborloko, mi preparis kaj subtenis doktora diplomo en CEA List kaj ENS, enkadrate de Matthieu Lemerre kaj Xavier Rival. Ĝi estas pri statika analizado de malaltnivela kodo por kontroli la sekureco de kernoj (inter aliaj). Post tiu doktordiplomo, mi laboris dum 4 jaroj en Tarides sur la programlingvo OCaml kaj ĝia ekosistemo.
Krom statika analizado, ankaŭ interesas min la funkcia programado, tipsistemoj kaj logiko.
Mia nomo prononciĝas ɔ.li'vje ni'kol, sed mi ne tro zorgas se vi prononcas ĝin “Oliver” aŭ iel ajn sufiĉe proksime por ke mi komprenu.
Personaj projektoj
- Mi kontribuis enkodigi la tipografion de matematiko en la tipografiilon SILE.
- haskell-chess: iu ridinde simpla kaj nekompleta ŝakprogramo en Haskell. Eble iam mi kompletigos ĝin.
- spino: provo enkodigi la logika strukturo de la Etiko de Spinoza en la pruvlingvaĵo Agda. Tiu laboro baziĝas sur Jarrett, The logical structure of Spinoza's Ethics, Part I.
Komunikaĵoj
- Runtime Detection of Data Races in OCaml with ThreadSanitizer (longa resumo) (lumbildoj) (video, mi bedaŭras pri la malbonegan sonon)
Olivier Nicole kaj Fabrice Buoro
OCaml Workshop 2023 - Multicoretests – Parallel Testing Libraries for OCaml 5.0 (longa resumo)
Jan Midtgaard, Olivier Nicole kaj Nicolas Osborne
OCaml Workshop 2022 -
Automatically Proving Microkernel Security
(lumbildoj,
franclingva video)
Olivier Nicole
RESSI 2020 (Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information), mallonga artikolo -
Modular Macros (Afiŝo/Montrado) (pdf)
Olivier Nicole, Leo White kaj Jeremy Yallop
PEPM 2018
Eldonaĵoj
-
MacoCaml: Staging Composable and Compilable Macros
(artikolo)
Ningning Xie, Leo White, Olivier Nicole kaj Jeremy Yallop
ICFP 2023 (International Conference on Functional Programming) -
Lightweight Shape Analysis based on Physical Types
(antaǔeldonaĵo)
Olivier Nicole, Matthieu Lemerre, Xavier Rival
VMCAI 2022 (Verification, Model Checking and Abstract Interpretation) -
No Crash, No Exploit: Automated Verification of Embedded Kernels
(antaǔeldonaĵo)
(reproduktilo)
(video de la prezento)
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
RTAS 2021 (IEEE Real-Time and Embedded Technology and Applications Symposium)
Best Paper Award
Doktora disertaĵo
Automated Verification of Systems Code using Type-based Memory Abstractions
- PDF por ekranoj, por printi (ligiloj ne koloritaj)
- Video de la disertado (angle)
Instruado
2020–2021
- Matematiko S1: Bazoj de la logiko. L1-livelo, CRI Paris (12 h)
- Mathematiko S2: Lineara algebro. L1-livelo, CRI Paris (12 h)
2019–2020
- Éléments de programmation (Eroj da programado) — LU1IN001. L1-livelo, Sorbonne Université (19 h)
- Programmation en C (C-programado) — PRC05. L3-livelo, École d'ingénieurs Denis Diderot, Université Paris 7 (27 h)
2018–2019
- Systèmes d'exploitations (Operaciumoj) — IN201. M1-livelo, ENSTA Paris, (15 h)
