About me
I am a PhD student, since October 2024, at the LIPN laboratory in the LoCal team. I am supervised by Marie Kerjean and Stefano Guerrini.
I am interested in the links between logical and mathematical structures through the Curry-Howard-Lambek correspondance. My favorite subject is categorical semantics of logic. I find it very beautiful when logical systems are able to describe complex and non discrete mathematical object, the most famous example being Homotopy type theory and my favorite one being convenient vector spaces as models of DiLL. My research focuses on the links between categorical models of DiLL (Differential Linear Logic) and (dependent) type theory.
More broadly, I like (in no particular order): Type Theory, Categorical Logic, Differential Linear Logic, Topology, Proof Theory, Category Theory, Homotopy Theory, Choice axioms, Realizabilty, Functional Analysis and Differential Geometry.
Contact :
- Email : koleilat at lipn.univ-paris13.fr
- Office : B311 - LIPN, Institut Galilée - Université Sorbonne Paris Nord, 99 avenue Jean-Baptiste Clément, 93430 Villetaneuse
Research
Publications :
- "On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles" in colaboration with Hugo Herbelin, FSCD 2024. [paper | HAL version]
Research internships :
Before starting a PhD, I did a few research internships:
- "A monadic approach to differentiation" supervised by Marie Kerjean, 2024. [pdf]
- "Classical Realizability : Models of PAω + DC" supervised by Guillaume Geoffroy, 2023. [pdf English | pdf Français]
- "Théories des types et paradoxe de Girard" supervised by Christine Paulin-Mohring, 2022. [pdf Français]
Talks
- "A Tangent on Categorical Models of Differential Linear Logic", TLLA 2025, July 2025. [abstract | web site]
-
"A Tangent on Categorical Models of Differential Linear Logic", LHC, June 2025. [slides | web site]
Abstract
We give a more functorial presentation of categorical models of differential linear logic as a linear-non-linear adjunction equipped with a linear tangent functor. This work is in the spirit of the the work of Kerjean, Maestracci and Rogger on a functorial characterization of categorical models of DiLL. Our approach is inspired by categorical semantics of type theory : given any linear-non-linear adjunction we construct a category called the linear-non-linear simple category which is the linear-non-linear equivalent of the simple slice category and is a fibration above the cartesian category. This category plays a crucial role in our axiomatisation and is the logical counter-part of the trivial vector bundle category. This adds to the already present intuition that linear logic should be the logical counter part of (trivial) vector bundle.
Teaching
2024-2025 :
- TD-TP Programmation Impérative 1 (en C) [L1 semestre 1]
- TD-TP Compilation (en Ocaml) [L3 semestre 2]
2025-2026 :
- TD-TP Programmation Impérative 3 (en C) [L2 semestre 1]
- Séminaire de catégories [L3 semestre 1]
Miscellaneous
This website is inspired by this series of websites: motherfuckingwebsite, bettermotherfuckingwebsite, evenbettermotherfuckingwebsite, perfectmotherfuckingwebsite.
I like and follow this blog (in french).
A funny meme (original post) :
