Experience

/ 1 MIN READ

Homotopy Type Theory

I took an internship at the LIX studying Homotopy Type Theory, supervised by Samuel Mimram and Emile Oléon. During this internship I used the Agda proof assistant to show a minimal construction for generated group deloopings. This led me to co-author a short paper on the topic, submited at the JFLA.

Quantum Optics

I took a second internship at the Quantum Optics team of the Universidad de los Andes in Bogota, Colombia. Supervised by Alonso Botero, we studied the semi-classical behaviour of multi-port interferometers on non-interacting indistinguishable bosons. The aim was to study the case of many particles to understand potential applications towards quantum supremacy. Though I plan to pursue a thesis in the field of my first intership, this one helped me discover research through the lens of physics which to me was an invaluable experience.

Oral examiner in mathematics

I've been working for 2 years as an oral examiner for preparatory classes at the Lycée La Martinière Monplaisir, in the MP* class (Math curriculum). I deliver two 1h examinations a week for three students at a time.

Programming and Software

I am proficient with the following software:

  • Lean proof assistant
  • Python programming language
  • OCaml programming language
  • Latex typesetting language

I am very familiar with the following:

  • Agda proof assistant
  • Coq proof assistant
  • Rust programing language

Some of my spare-time projects include a fractal explorer in Rust, a lambda-calculus interpreter in OCaml, and a music-practice website.