Jad Koleilat

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 :

Research

Preprints:

• "A Fibrational Perspective on Differential Linear Logic". [Arxiv]

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

2026:

• "A Fibrational Perspective on Differential Linear Logic", Differentiation in category theory and program semantics, Kyoto, April 2026. [slides | web site]
  Abstract

  Differential Linear Logic (DiLL) is a sequent calculus expressing differentiation through symmetries between linear and non-linear formulas. In this talk, we express categorical models of DiLL as a pair of Grothendieck fibrations equipped with a tangent functor. To do so, we adapt methods from categorical semantics of type theory to linear-non-linear adjunctions. In the future, we hope this approach will enable the construction of models of what could be called dependent differential linear logic.

2025:

• "A Fibrational Perspective on Differential Linear Logic", Aix-Marseille Université, I2M, Marseille, October 2025. [slides]
  Abstract

  Differential Linear Logic (DiLL) is a sequent calculus expressing differentiation through symmetries between linear and non-linear formulas. In this paper, we express categorical models of DiLL as a pair of Grothendieck fibrations equipped with a tangent functor. To do so, we adapt methods from categorical semantics of Type Theory to linear-non-linear adjunctions. In the future, we hope this approach will enable the construction of models of a flavor of dependent differential linear logic.
• "A Tangent on Categorical Models of Differential Linear Logic", TLLA 2025, Birmingham, July 2025. [abstract | web site]
• "A Tangent on Categorical Models of Differential Linear Logic", LHC, Paris, 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.

A funny meme (original post) :