I am a 4th year student at Ens Paris-Saclay in theoretical computer science. I am currently working with Benedikt Ahrens on a unified framework for initial semantics, and with Ambroise Lafont on leveraging the parametricity of such frameworks in the input category.
My main interests are :
- Type Theory
- Proof Assistants
- Functional Programming Languages
- Categorical Semantics
I will give at talk at the workshop Homotopy Type Theory and Computing - Classical and Quantum entitled “Computing Cohomology Rings in Cubical Agda” about our associated CPP paper.
I will be starting my master 2 research internship in march 2024, under the supervision of Nicolas Tabareau. We will investigate the generation of induction principles for nested inductive types in Coq.
I am happy to share our new preprint An Introduction to Different Approaches to Initial Semantics with Benedikt Ahrens, that aims at getting closer different approaches to initial semantics.
In the paper, we explain how to formalize Cohomology Rings in synthetic mathematics. With a special focus on data structures and how they influence formalization, most noticeably the direct sum and (multivariate) polynomials.