LOMay 8
A Fibrational Perspective on Differential Linear Logic
arXiv:2605.0785815.9
Predicted impact top 48% in LO · last 90 daysOriginality Incremental advance
AI Analysis
For researchers in categorical logic and type theory, this offers a foundational framework but is an incremental step toward a known goal.
This paper provides a new categorical semantics for Differential Linear Logic (DiLL) using Grothendieck fibrations and a tangent functor, aiming to unify DiLL with dependent types.
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.