About me

Depending on viewing conditions, a computer science student with a background in physics, or a lost physicist happily wandering through type and category theory.

Status

As of September 2025, I have completed the MPRI master's program and obtained a master's degree in computer science. I will spend the 2025/2026 academic year in internships in industry and/or academia, in order to scout out career possibilities before committing to a PhD. Administratively, I remain a student at ENS Paris.

Contact

• Email me at simon.dima@normalesup.org, in English, French or German
• Track my contributions to science: ORCID

Education

In addition to the MPRI master's degree in computer science, I have obtained bachelor's degrees in mathematics (2023) and physics (2022), both from École Normale Supérieure. Before ENS, I followed the PSI track of classe préparatoire at Louis-le-Grand.

Internships

Compiling Lean programs with Rocq's extraction pipeline (2025—03/08)

Five-month research internship supervised by Yannick Forster at the Cambium group of Inria Paris.
Investigated the different tradeoffs made by Lean's compiler, which targets C, and Rocq's verified extraction pipeline, which targets the OCaml compiler's intermediate representation.

• Implemented a bridge from Lean's term language into Rocq's verified extraction pipeline.
• Added support for features which are handled specially by the Lean compiler, such as persistent arrays and fast integer arithmetic.
• Measured the influence of various configuration options on the performance of generated executables with a small set of benchmark programs.

Links: internship report, source code.

SatisfIA research project (2024—03/08)

Project investigating alternatives to maximization-based planning for safer AI agents.
Five-month research internship supervised by Jobst Heitzig at PIK Potsdam.
What I did:

• Wrote a few blog posts, including an analysis of toy models of damages from misaligned optimization and an explanation of the formal framework of the SatisfIA project and of a simple algorithm guaranteeing one-dimensional expected results.
• Helped develop an algorithm ensuring expected results in multidimensional Markov Decision Processes, published in a paper presented at the 2024 International Conference on Algorithmic Decision Theory.

CASPEr-Gradient experiment (2022—06/07)

Axion-like dark matter search experiment via Nuclear Magnetic Resonance with hyperpolarized xenon.
One-month internship supervised by Hendrik Bekker and Dmitry Budker at the MAM section of Helmholtz Institute Mainz.
What I did:

• Built a 16-channel relay control system for manual and automatic switching of valves, including adaptation of the existing LabVIEW interface and writing documentation for the new hardware.
• Set up an automated liquid nitrogen refilling system with capacitive level sensing.