Carrefour China - 家乐福中国 — 2018-2019

I worked almost a year in Shanghai for Carrefour China, the Chinese branch of the French retailer, on the development of data offers and data partnerships. I supervised the design and implementation of Business Intelligence products by the IT team, recruited data-analysts, negotiated with suppliers and partners, and handled contract drafting and signature.

Prove & Run — 2017-2018

I worked for 9 months at Prove & Run on ProvenTools ®, an environment to develop mathematically verified programs in an industrial setting. My task was to design and implement a mechanism in Java to embed the programs written and verified with ProvenTools ® into the logic of the Coq proof assistant.

The goal of the project was to improve the confidence one can have in the programs verified with ProvenTools ®, by giving the possibility to use a widely-known and trusted proof assistant to independently recheck the properties proven about those programs.

CakeML, CSIRO’s Data61 — 2017

During my master internship, I worked on the CakeML project, which aims at developing a framework to write SML programs verified down to the compiled executables by using the HOL4 theorem prover. I worked on a mechanism which automatically synthesizes stateful ML code from functions written in the logic of the HOL4 theorem prover, while generating a proof that the synthesized ML code correctly implements the functions defined in HOL4. Our results were published at IJCAR2018, and the slides are available here.

IDEMIA — 2016

During my second year at École polytechnique, I did an internship at IDEMA, one of the world leaders in biometrics, to develop semi-automated image labelling tools in Python.

The goal of such tools is to speed-up the work of classifying images (say: giving the labels “cat”, “dog”, “horse”, etc. to images of animals) in order to generate training datasets for machine-learning algorithms, by learning the classification while the user is working on it and using this knowledge to assist him in doing so.

In practice, by using the tools I implemented, one could label tens of thousands of images per hour without much effort.