index.en.html

---
title: Home
---

<h2>Olivier Nicole</h2>

<p>
Hello, I’m Olivier. During daytime, I work for Tarides on <a
  href="https://ocaml.org/">the OCaml language</a>, 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 <a
href="https://github.com/OlivierNicole">my Github profile</a>.
</p>

<p>
Part of the rest of my time is spent reading philosophy or various novels (with
an inclination toward SF), or hacking on a <a
href="https://github.com/sile-typesetter/sile">typesetting software</a>.
</p>

<p>
Before my current job, I did a PhD at <a
  href="http://www-list.cea.fr/en/technological-research/research-programmes/embedded-systems/validation-and-verification">CEA
  List</a> and <a href="https://www.ens.fr/en">ENS</a> 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).
</p>

<p>I'm also interested in functional programming, type systems and logic.</p>

<p>My name is pronounced <span class="pronunciation">ɔ.li'vje ni'kol</span>,
but “Oliver” with the usual English pronunciation is also fine.</p>

<h2>Personal projects</h2>

<ul>
  <li>I have contributed to implement mathematics typesetting into the <a href="https://github.com/sile-typesetter/sile">SILE</a> typesetter.</li>
  <li><a
      href="https://github.com/OlivierNicole/haskell-chess">haskell-chess</a>:
    a ridiculously simple and incomplete chess engine in Haskell. May be
    completed some day.</li>
  <li><a href="https://github.com/OlivierNicole/spino">spino</a>: an attempt to
    encode the logical structure of Spinoza’s “Ethics” in the proof language
    Agda. The work is based on 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">extended abstract</a>) (<a href="/papers/ocaml_2023_tsan.pdf">slides</a>) (<a href="https://www.youtube.com/watch?v=zr9S0Fr_Chc&list=PLyrlk8Xaylp7Tq5-ZN6jkir-sYrhGi_0E&index=3">video</a>, sorry about the terrible sound)<br />
    Olivier Nicole and 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">extended abstract</a>) (<a href="https://watch.ocaml.org/w/qJm8mKUgCr1KroxXiQXgLZ">video</a>)<br />
    Jan Midtgaard, Olivier Nicole and 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">slides</a>,
      <a href="/talks/ressi_2020.mp4">video in French</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/Demo Talk) (<a
      href="/papers/PEPM18-Modular-Macros.pdf">pdf</a>)<br />
    Olivier Nicole, Leo White and 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">paper</a>)
    <br />
    Ningning Xie, Leo White, Olivier Nicole and 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">artifact</a>)
    (<a href="https://www.youtube.com/watch?v=668VgDJy2ZI">presentation video</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="Badge icon">Best Paper Award</span>
  </li>
</ul>

<h2 id="thesis">PhD thesis</h2>

<p><strong>Automated Verification of Systems Code using Type-based Memory
Abstractions</strong></p>

<ul>
  <li><a href="/papers/thesis.pdf">PDF for screens</a>, <a
      href="/papers/thesis_for_printing.pdf">for printing</a> (hyperlinks not
    colored)</li>
  <li><a href="https://www.youtube.com/watch?v=nl-hG5vQE2E">Video of the
      defense</a> (in English)</li>
</ul>

<h2>Teaching</h2>

<h3>2020–2021</h3>

<ul>
  <li><a href="teaching/fdv2020/index.html">Mathematics S1: Elementary
  logic</a>. L1 level, CRI Paris (12 h)</li>
  <li><a href="teaching/fdv2020_s2/index.html">Mathematics S2: Linear algebra</a>.
  L1 level, CRI Paris (12 h)</li>
</ul>

<h3>2019–2020</h3>

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

<h3>2018–2019</h3>

<ul>
  <li>Systèmes d'exploitations (Operating Systems) — IN201. M1 level, ENSTA
    Paris (15 h)</li>
</ul>