Document Open Access Logo

Functorial Models of Differential Linear Logic

Authors Marie Kerjean , Valentin Maestracci , Morgan Rogers

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.26.pdf
  • Filesize: 1.35 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.26.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Denotational semantics
  • Theory of computation → Linear logic
Keywords
  • Categorical semantics
  • Differential Programming
  • Linear Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Differentiation in logic has several sources of inspiration. The most recent is differentiable programming, models of which demand functoriality and good typing properties. More historical is reverse denotational semantics, taking inspiration from models of Linear Logic to differentiate proofs and λ-terms. In this paper, we take advantage of the rich structure of categorical models of Linear Logic to give a new functorial presentation of differentiation. We define differentiation as a functor from a coslice of the category of smooth maps to the category of linear maps. Extending linear-non-linear adjunction models of Linear Logic, this produces models of Differential Linear Logic. We use these functorial presentations to shed new light on integration in differential categories.

Cite As Get BibTex

Marie Kerjean, Valentin Maestracci, and Morgan Rogers. Functorial Models of Differential Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.26

Author Details

Marie Kerjean
  • CNRS, Université Sorbonne Paris Nord, Laboratoire d'Informatique de Paris Nord, LIPN, F-93430 Villetaneuse, France
Valentin Maestracci
  • Aix-Marseille Université, CNRS, I2M, France
Morgan Rogers
  • Université Sorbonne Paris Nord, CNRS, Laboratoire d'Informatique de Paris Nord, LIPN, F-93430 Villetaneuse, France

Funding

  • Kerjean, Marie: Work partially funded by the project ANR-24-CE48-1914.

Acknowledgements

We are grateful to Jean-Simon Lemay, Zeinab Galal, and Jad Koleilat for enriching discussions on this paper. We also thank the reviewers for the many constructive comments, helping us making this paper a better version of itself

References

  1. R. F. Blute, J. R. B. Cockett, J.-S. P. Lemay, and R. A. G. Seely. Differential categories revisited. Applied Categorical Structures, 2020. URL: https://doi.org/10.1007/s10485-019-09572-y.
  2. R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. Differential categories. Mathematical Structures in Computer Science, 2006. URL: https://doi.org/10.1017/S0960129506005676.
  3. R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. Cartesian differential categories. Theory and Applications of Categories, 2009. Google Scholar
  4. Richard Blute, Thomas Ehrhard, and Christine Tasson. A convenient differential category. Cahiers de topologie et géométrie différentielle catégoriques, 53(3):211-232, 2012. URL: https://arxiv.org/abs/1006.3140.
  5. A. Brunel, D. Mazza, and M. Pagani. Backpropagation in the Simply Typed Lambda-calculus with Linear Negation. POPL, 2020. URL: https://doi.org/10.1145/3371132.
  6. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Computer Science Logic, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_24.
  7. J. R. B. Cockett and J.-S. Lemay. Integral categories and calculus categories. Mathematical Structures in Computer Science, 29:243-308, 2019. URL: https://doi.org/10.1017/S0960129518000014.
  8. J. Robin B. Cockett and Geoff S. H. Cruttwell. Differential Structure, Tangent Structure, and SDG. Appl. Categorical Struct., 22(2):331-417, 2014. URL: https://doi.org/10.1007/s10485-013-9312-0.
  9. J. Robin B. Cockett, Geoff S. H. Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon D. Plotkin, and Dorette Pronk. Reverse derivative categories. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 18:1-18:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.18.
  10. Y. Dabrowski and M. Kerjean. Models of Linear Logic based on the Schwartz ε product. Theory and Applications of Categories, 2020. URL: https://doi.org/10.48550/arXiv.1712.07344.
  11. T. Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Math. Struct. Comput. Sci., 2017. URL: https://doi.org/10.1017/S0960129516000372.
  12. T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2), 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.003.
  13. Conal Elliott. The simple essence of automatic differentiation. In Proceedings of the ACM on Programming Languages (ICFP), 2018. URL: https://doi.org/10.1145/3236765.
  14. M. P. Fiore. Differential structure in models of multiplicative biadditive intuitionistic linear logic. In TLCA, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_13.
  15. J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50(1), 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  16. Marie Kerjean. A logical account for linear partial differential equations. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 589-598. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209192.
  17. Paul-André Mellies. Categorical semantics of linear logic. Société Mathématique de France, 2008. Google Scholar
  18. L. Schwartz. Théorie des distributions. Hermann, Paris, 1966. Google Scholar
  19. R. A. G. Seely. Linear Logic, *-Autonomous Categories and Cofree Coalgebras. In In Categories in Computer Science and Logic. American Mathematical Society, 1989. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact