A Fibrational Perspective on Differential Linear Logic
Logic in Computer Science
2026-05-11 v1
Abstract
Differential Linear Logic (DiLL) is a sequent calculus that expresses differentiation via 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. This is a first step towards unifying DILL and dependent types.
Cite
@article{arxiv.2605.07858,
title = {A Fibrational Perspective on Differential Linear Logic},
author = {Jad Koleilat},
journal= {arXiv preprint arXiv:2605.07858},
year = {2026}
}