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 April 2025, I am working on extraction from proof assistants during a research internship with Yannick Forster. This internship is the last part of the MPRI master's program, which I am completing as part of my studies at ENS Paris.

Contact

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

Internships

Extraction of code from proof assistants (2025—03/08, ongoing)

Supervised by Yannick Forster at the Cambium group of Inria Paris.

Goals: implementing/hacking together extraction

• from Lean to OCaml, using Rocq's existing extraction pipeline
• from Rocq to C, using Lean's compilation pipeline
• from Rocq to CakeML,

and measuring, comparing, and understanding the performance of the various extractions.

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. Stuff 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.
Stuff 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.

Education

In addition to my soon-to-be-completed master's degree in computer science, I have bachelor's degrees in mathematics and physics, both from ENS.

Before ENS, I followed the PSI track of classe préparatoire at Louis-le-Grand.