index.eo.html

---
title: Hejma paĝo
---

<h2>Olivier Nicole</h2>

<p>Saluton, mi nomiĝas Olivier. Tagtempe, mi laboras por la firmo Tarides sur <a
  href="https://ocaml.org/">la programlingvo OCaml</a>, 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 <a href="https://github.com/OlivierNicole">mia Github-profilo</a>.
</p>

<p>
Cetertempe, mi legas filozofion aŭ diversaj romanoj (kun ŝatado por la SF), aŭ
mi kelkaŭtempe kodumas en <a
  href="https://github.com/sile-typesetter/sile">tipografia programaro</a>.
</p>

<p>
Antaŭ mia nuna laborloko, mi preparis kaj subtenis doktora diplomo en <a
  href="http://www-list.cea.fr/en/technological-research/research-programmes/embedded-systems/validation-and-verification">CEA
  List</a> kaj <a href="https://www.ens.fr/en">ENS</a>, enkadrate de Matthieu Lemerre kaj Xavier
Rival.
Ĝi estas pri statika analizado de malaltnivela kodo por kontroli la sekureco de
kernoj (inter aliaj).
</p>

<p>Krom statika analizado, ankaŭ interesas min la funkcia programado,
tipsistemoj kaj logiko.</p>

<p>Mia nomo prononciĝas <span class="pronunciation">ɔ.li'vje ni'kol</span>,
sed mi ne tro zorgas se vi prononcas ĝin “Oliver” aŭ iel ajn sufiĉe proksime
por ke mi komprenu.</p>

<h2>Personaj projektoj</h2>

<ul>
  <li>Mi kontribuis enkodigi la tipografion de matematiko en la tipografiilon <a href="https://github.com/sile-typesetter/sile">SILE</a>.</li>
  <li><a
      href="https://github.com/OlivierNicole/haskell-chess">haskell-chess</a>:
    iu ridinde simpla kaj nekompleta ŝakprogramo en Haskell. Eble iam mi
    kompletigos ĝin.</li>
  <li><a href="https://github.com/OlivierNicole/spino">spino</a>: provo enkodigi la logika strukturo de la Etiko de Spinoza en la pruvlingvaĵo Agda. Tiu laboro baziĝas 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">Komunikaĵoj</h2>

<ul>
  <li><strong>Runtime Detection of Data Races in OCaml with ThreadSanitizer</strong> (<a href="/papers/ocaml_2023_tsan_abstract.pdf">longa resumo</a>) (<a href="/papers/ocaml_2023_tsan.pdf">lumbildoj</a>) (<a href="https://www.youtube.com/watch?v=zr9S0Fr_Chc&list=PLyrlk8Xaylp7Tq5-ZN6jkir-sYrhGi_0E&index=3">video</a>, mi bedaŭras pri la malbonegan sonon)<br />
    Olivier Nicole kaj 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">longa resumo</a>)<br />
    Jan Midtgaard, Olivier Nicole kaj 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">lumbildoj</a>,
      <a href="/talks/ressi_2020.mp4">franclingva video</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), mallonga artikolo
  </li>
  <li>
    <strong>Modular Macros</strong> (Afiŝo/Montrado) (<a
      href="/papers/PEPM18-Modular-Macros.pdf">pdf</a>)<br />
    Olivier Nicole, Leo White kaj 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">Eldonaĵoj</h2>

<ul>
  <li>
    <strong>MacoCaml: Staging Composable and Compilable Macros</strong>
    (<a href="/papers/icfp_2023_macros.pdf">artikolo</a>)
    <br />
    Ningning Xie, Leo White, Olivier Nicole kaj 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">antaǔeldonaĵo</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">antaǔeldonaĵo</a>)
    (<a href="https://github.com/binsec/rtas2021_artifact">reproduktilo</a>)
    (<a href="https://www.youtube.com/watch?v=668VgDJy2ZI">video de la prezento</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="Medala piktogramo">Best Paper Award</span>
  </li>
</ul>

<h2 id="thesis">Doktora disertaĵo</h2>

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

<ul>
  <li><a href="/papers/thesis.pdf">PDF por ekranoj</a>, <a
         href="/papers/thesis_for_printing.pdf">por printi</a> (ligiloj ne
       koloritaj)</li>
  <li><a href="https://www.youtube.com/watch?v=nl-hG5vQE2E">Video de la
      disertado</a> (angle)</li>
</ul>

<h2>Instruado</h2>

<h3>2020–2021</h3>

<ul>
  <li><a href="teaching/fdv2020/index.html">Matematiko S1: Bazoj de la logiko</a>. L1-livelo, CRI Paris (12 h)</li>
  <li><a href="teaching/fdv2020_s2/index.html">Mathematiko S2: Lineara algebro</a>. L1-livelo, CRI Paris (12 h)</li>
</ul>

<h3>2019–2020</h3>

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

<h3>2018–2019</h3>

<ul>
  <li>Systèmes d'exploitations (Operaciumoj) — IN201. M1-livelo, ENSTA Paris,
    (15 h)</li>
</ul>