News
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