Research & Implementation
PhD Research
Thesis Advisor : Samuel Mimram
My PhD research focuses on the theoretical foundations of computer-assisted proofs, and more specifically on Homotopy Type Theory (HoTT), a logical paradigm with a topological flavor.
​
In this context, I explore how structures can be represented in a coherent way—favoring deep embeddings over shallow ones.
Some of my results have been formally verified using the Agda proof assistant.
research articles:
-
Coherent Tietze transformations of 1-polygraphs in HoTT
S.Mimram and E.Oleon
Accepted at FSCD'25
paper here.
​
-
Delooping cyclic groups with lens spaces in HoTT
S.Mimram and E.Oleon
Accepted at LICS'24
https://arxiv.org/abs/2405.10149
​
-
Delooping generated groups in HoTT
C.Champin, S.Mimram and E.Oleon
Accepted at FSCD'24
https://arxiv.org/abs/2405.03264
​
Bonus
​there is more depth to division by two than you may think ...
building a constructive variant of this operation on types is actually a tricky combinatorics problem !