I am a software engineer with a PhD in type theory. I am specialised in statically-typed functional languages and I like to use the right abstractions to develop robust software.

Currently, I am also interested in machine learning as I believe this technology has a great transformative potential with respect to society.

More generally, my interests lie in the scientific methods devised to produce and exploit knowledge. I did my PhD in type theory, a formal language used to represent and make precise mathematical statements and their proofs, and I now am interested in using quantitative methods, such as machine learning, to enquire questions about the real world. These domains are different but they revolve around the central theme of representing and harnessing knowledge.

Research

Previously, I did my PhD on the open problem of defining coherent algebraic structures in homotopy type theory (HoTT) in the Inria team Picube at IRIF located at Université Paris Cité under the supervision of Dr. Matthieu Sozeau and in collaboration with Dr. Eric Finster.

My research focused on an extension of HoTT allowing the definition of coherent algebraic structures on types, and relatedly, making possible the development of basic higher category theory in a synthetic fashion by exploiting the higher dimensional structure of types.

You can read my PhD thesis. Most of the results have been formalised in the Agda proof assistant. Part of my work was the subject of an article accepted at LICS 2021.

More generally, I am interested in the connections between type theory, category theory, and programming languages (the computational trilogy).

Contact

You can send me an email.