News
I will give a talk at the WorkGroup 6’s meeting entitled “A Unified Framework for Initial Semantics, and it is 2-Functorial” about our work with Benedikt Ahrens and Ambroise Lafont to unify and relate different approaches to initial semantics.
I am happy to share a significantly improved second draft of “An Introduction to Different Approaches to Initial Semantics”, A Unified Framework for Initial Semantics with Benedikt Ahrens, that aims at getting closer different approaches to initial semantics.
I am happy to announce I am starting a PhD with in the Gallinette team at Inria & Nantes University, under the direction of Nicolas Tabareau, Yannick Forster, and Matthieu Sozeau. I will be working on Proof Assistants, most particularly on generating recursors for (nested) inductive types using MetaCoq, and towards formalising Coq’s guard condition.
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.
I will give at talk at Stockholm University’s Logic Seminar. about unifying different approaches to Initial Semantics.
I will give at talk at the workshop Dutch Categories And Types Seminar entitled “Introduction and comparison of different approaches to Initial Semantics”, in which we will discuss the different approaches and how they relate.
Our paper Computing Cohomology Rings in Cubical Agda with Axel Ljungström and Anders Mörtberg, was accepted at CPP 2023 and awarded Distinguished Paper.
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.
As my 3rd at Ens Paris-Saclay, I am starting in October 2022, a 9 months research internship with Benedikt Ahrens. The project will be to extend the framework of initial semantics (in the tradition of monads-based models) with polymorphism.
I will give a talk about Univalent Relational Parametricity at the Logic Seminar of the Logic Group at Stockholm University on the 6th April 2022.
For my second semester of first year of Master, I will do a 6 months research internship with Anders Mörtberg. The project will be to attempt to formalize cohomology rings, in univalent synthetic mathematics in Cubical Agda
For my last year of bachelor, I will do a 2 months research internship with Nicolas Tabareau. The project will be to reformulate the framework of univalent parametricity to fully size to CIC omega