index.fr.html

---
title: Accueil
---

<h2>Olivier Nicole</h2>

<p>Bonjour, je m’appelle Olivier. En journée, je travaille pour Tarides sur <a
  href="https://ocaml.org/">le langage OCaml</a> 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 <a href="https://github.com/OlivierNicole">mon profil
Github</a>.

<p>
Le reste du temps, je lis de la philo ou divers romans (avec un penchant
pour la SF), ou je hacke de temps en temps sur <a
href="https://github.com/sile-typesetter/sile">un logiciel de typographie</a>.
</p>

<p>Avant mon emploi actuel, j'ai préparé et soutenu un doctorat au <a
  href="http://www-list.cea.fr/en/technological-research/research-programmes/embedded-systems/validation-and-verification">CEA
  List</a> et à <a href="https://www.ens.fr/en">l’ENS</a> 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).</p>

<p>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.</p>

<h2>Projets personnels</h2>

<ul>
  <li>J’ai contribué à implémenter le rendu des mathématiques dans le logiciel
    typographique <a href="https://github.com/sile-typesetter/sile">SILE</a>.
  </li>
  <li><a
      href="https://github.com/OlivierNicole/haskell-chess">haskell-chess</a>:
    un moteur d’échecs ridiculement simple, et incomplet. Sera peut-être
    terminé un jour.</li>
  <li><a href="https://github.com/OlivierNicole/spino">spino</a>: une tentative
     (incomplète) d’encoder la structure logique de <em>L’Éthique</em> de
     Spinoza dans le langage de preuve Agda. Le travail se base sur
       Jarrett, <a
    href="https://link.springer.com/article/10.1007/BF00869440">The logical
    structure of Spinoza's Ethics, Part I</a>.</li>
</ul>

<h2 id="com">Communications</h2>

<ul>
  <li><strong>Runtime Detection of Data Races in OCaml with ThreadSanitizer</strong> (<a href="/papers/ocaml_2023_tsan_abstract.pdf">résumé long</a>) (<a href="/papers/ocaml_2023_tsan.pdf">diapos</a>) (<a href="https://www.youtube.com/watch?v=zr9S0Fr_Chc&list=PLyrlk8Xaylp7Tq5-ZN6jkir-sYrhGi_0E&index=3">vidéo</a>, désolé pour la mauvaise qualité du son)<br />
    Olivier Nicole et Fabrice Buoro<br />
    <a href="https://icfp23.sigplan.org/home/ocaml-2023#">OCaml Workshop 2023</a>
  </li>
  <li><strong>Multicoretests – Parallel Testing Libraries for OCaml 5.0</strong> (<a href="/papers/ocaml_2022_multicoretests.pdf">résumé long</a>)<br />
    Jan Midtgaard, Olivier Nicole et Nicolas Osborne<br />
    <a href="https://v3.ocaml.org/workshops/ocaml-workshop-2022">OCaml Workshop 2022</a>
  </li>
  <li>
    <strong>Automatically Proving Microkernel Security</strong>
      (<a href="/talks/ressi_2020.pdf">diapos</a>,
      <a href="/talks/ressi_2020.mp4">vidéo</a>)
    <br />
    Olivier Nicole <br />
    <a href="https://ressi2020.sciencesconf.org/">RESSI 2020</a> (Rendez-vous
    de la Recherche et de l'Enseignement de la Sécurité des Systèmes
    d'Information), short paper
  </li>
  <li><strong>Modular Macros</strong> (Poster/Démonstration) (<a href="/papers/PEPM18-Modular-Macros.pdf">pdf</a>)<br />
    Olivier Nicole, Leo White et Jeremy Yallop<br />
    <a href="https://popl18.sigplan.org/event/pepm-2018-modular-macros-poster-demo-talk-">PEPM 2018</a>
  </li>
</ul>

<h2 id="pub">Publications</h2>

<ul>
  <li>
    <strong>MacoCaml: Staging Composable and Compilable Macros</strong>
    (<a href="/papers/icfp_2023_macros.pdf">article</a>)
    <br />
    Ningning Xie, Leo White, Olivier Nicole et Jeremy Yallop <br />
    <a href="https://icfp23.sigplan.org/">ICFP 2023</a> (International Conference on Functional Programming)
  </li>
  <li>
    <strong>Lightweight Shape Analysis based on Physical Types</strong>
    (<a href="/papers/vmcai22_lightweight_shape_analysis.pdf">pre-print</a>)
    <br />
    Olivier Nicole, Matthieu Lemerre, Xavier Rival <br />
    <a href="https://popl22.sigplan.org/home/VMCAI-2022">VMCAI 2022</a> (Verification, Model Checking and Abstract Interpretation)
  </li>
  <li>
    <strong>No Crash, No Exploit: Automated Verification of Embedded Kernels</strong>
    (<a href="/papers/RTAS21-No-crash-no-exploit.pdf">pre-print</a>)
    (<a href="https://github.com/binsec/rtas2021_artifact">artefact</a>)
    (<a href="https://www.youtube.com/watch?v=668VgDJy2ZI">vidéo de la présentation</a>)
    <br />
    Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival <br />
    <a href="http://2021.rtas.org/">RTAS 2021</a> (IEEE Real-Time and Embedded Technology and Applications Symposium) <br />
    <span class="award"><img src="vendor/img/medal.png" alt="Icône de médaille">Best Paper Award</span>
  </li>
</ul>

<h2 id="thesis">Thèse</h2>

<p><strong>Vérification automatisée de code système à l’aide d’abstractions
  mémoire basées sur le typage</strong></p>

<ul>
  <li><a href="/papers/thesis.pdf">PDF pour lecture sur écran</a>, <a
         href="/papers/thesis_for_printing.pdf">pour impression</a> (hyperliens
       non colorés)</li>
  <li><a href="https://www.youtube.com/watch?v=nl-hG5vQE2E">Soutenance</a> (en
    anglais)</li>
</ul>

<h2>Enseignement</h2>

<h3>2020–2021</h3>

<ul>
  <li><a href="teaching/fdv2020/index.html">Mathématiques S1: Bases de la logique</a>. L1, CRI Paris (12 h)</li>
  <li><a href="teaching/fdv2020_s2/index.html">Mathématiques S2: Algèbre linéaire</a>. L1, CRI Paris (12 h)</li>
</ul>

<h3>2019–2020</h3>

<ul>
  <li>Éléments de programmation — LU1IN001. L1, Sorbonne (19 h)</li>
  <li>Programmation en C — PRC05. L3, École d’ingénieurs Paris Diderot,
    Université Paris 7 (27 h)</li>
</ul>

<h3>2018–2019</h3>

<ul>
  <li>Systèmes d’exploitation — IN201. M1, ENSTA Paris (15 h)</li>
</ul>