6 Search Results for "Cockett, Robin"

Document
DOI: 10.4230/LIPIcs.CSL.2026.12
String Diagrams for Closed Symmetric Monoidal Categories

Authors: Callum Reader and Alessandro Di Giorgio

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.
Cite as

Callum Reader and Alessandro Di Giorgio. String Diagrams for Closed Symmetric Monoidal Categories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{reader_et_al:LIPIcs.CSL.2026.12,
  author =	{Reader, Callum and Di Giorgio, Alessandro},
  title =	{{String Diagrams for Closed Symmetric Monoidal Categories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.12},
  URN =		{urn:nbn:de:0030-drops-254369},
  doi =		{10.4230/LIPIcs.CSL.2026.12},
  annote =	{Keywords: diagrammatic languages, logic, lambda calculi}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.26
Functorial Models of Differential Linear Logic

Authors: Marie Kerjean, Valentin Maestracci, and Morgan Rogers

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{kerjean_et_al:LIPIcs.FSCD.2025.26,
  author =	{Kerjean, Marie and Maestracci, Valentin and Rogers, Morgan},
  title =	{{Functorial Models of Differential Linear Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.26},
  URN =		{urn:nbn:de:0030-drops-236419},
  doi =		{10.4230/LIPIcs.FSCD.2025.26},
  annote =	{Keywords: Categorical semantics, Differential Programming, Linear Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.17
Tangent Categories from the Coalgebras of Differential Categories

Authors: Robin Cockett, Jean-Simon Pacaud Lemay, and Rory B. B. Lucyshyn-Wright

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Following the pattern from linear logic, the coKleisli category of a differential category is a Cartesian differential category. What then is the coEilenberg-Moore category of a differential category? The answer is a tangent category! A key example arises from the opposite of the category of Abelian groups with the free exponential modality. The coEilenberg-Moore category, in this case, is the opposite of the category of commutative rings. That the latter is a tangent category captures a fundamental aspect of both algebraic geometry and Synthetic Differential Geometry. The general result applies when there are no negatives and thus encompasses examples arising from combinatorics and computer science.
Cite as

Robin Cockett, Jean-Simon Pacaud Lemay, and Rory B. B. Lucyshyn-Wright. Tangent Categories from the Coalgebras of Differential Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cockett_et_al:LIPIcs.CSL.2020.17,
  author =	{Cockett, Robin and Lemay, Jean-Simon Pacaud and Lucyshyn-Wright, Rory B. B.},
  title =	{{Tangent Categories from the Coalgebras of Differential Categories}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.17},
  URN =		{urn:nbn:de:0030-drops-116607},
  doi =		{10.4230/LIPIcs.CSL.2020.17},
  annote =	{Keywords: Differential categories, Tangent categories, Coalgebra Modalities}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.18
Reverse Derivative Categories

Authors: Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al., 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al., 2009] for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.
Cite as

Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, and Dorette Pronk. Reverse Derivative Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cockett_et_al:LIPIcs.CSL.2020.18,
  author =	{Cockett, Robin and Cruttwell, Geoffrey and Gallagher, Jonathan and Lemay, Jean-Simon Pacaud and MacAdam, Benjamin and Plotkin, Gordon and Pronk, Dorette},
  title =	{{Reverse Derivative Categories}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.18},
  URN =		{urn:nbn:de:0030-drops-116611},
  doi =		{10.4230/LIPIcs.CSL.2020.18},
  annote =	{Keywords: Reverse Derivatives, Cartesian Reverse Differential Categories, Categorical Semantics, Cartesian Differential Categories, Dagger Categories, Automatic Differentiation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.13
There Is Only One Notion of Differentiation

Authors: J. Robin B. Cockett and Jean-Simon Lemay

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Differential linear logic was introduced as a syntactic proof-theoretic approach to the analysis of differential calculus. Differential categories were subsequently introduce to provide a categorical model theory for differential linear logic. Differential categories used two different approaches for defining differentiation abstractly: a deriving transformation and a coderiliction. While it was thought that these notions could give rise to distinct notions of differentiation, we show here that these notions, in the presence of a monoidal coalgebra modality, are completely equivalent.
Cite as

J. Robin B. Cockett and Jean-Simon Lemay. There Is Only One Notion of Differentiation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cockett_et_al:LIPIcs.FSCD.2017.13,
  author =	{Cockett, J. Robin B. and Lemay, Jean-Simon},
  title =	{{There Is Only One Notion of Differentiation}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{13:1--13:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.13},
  URN =		{urn:nbn:de:0030-drops-77166},
  doi =		{10.4230/LIPIcs.FSCD.2017.13},
  annote =	{Keywords: Differential Categories, Linear Logic, Coalgebra Modalities, Bialgebra Modalities}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.20
Integral Categories and Calculus Categories

Authors: Robin Cockett and Jean-Simon Lemay

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Differential categories are now an established abstract setting for differentiation. The paper presents the parallel development for integration by axiomatizing an integral transformation in a symmetric monoidal category with a coalgebra modality. When integration is combined with differentiation, the two fundamental theorems of calculus are expected to hold (in a suitable sense): a differential category with integration which satisfies these two theorem is called a calculus category. Modifying an approach to antiderivatives by T. Ehrhard, it is shown how examples of calculus categories arise as differential categories with antiderivatives in this new sense. Having antiderivatives amounts to demanding that a certain natural transformation K, is invertible. We observe that a differential category having antiderivatives, in this sense, is always a calculus category and we provide examples of such categories.
Cite as

Robin Cockett and Jean-Simon Lemay. Integral Categories and Calculus Categories. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cockett_et_al:LIPIcs.CSL.2017.20,
  author =	{Cockett, Robin and Lemay, Jean-Simon},
  title =	{{Integral Categories and Calculus Categories}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.20},
  URN =		{urn:nbn:de:0030-drops-76687},
  doi =		{10.4230/LIPIcs.CSL.2017.20},
  annote =	{Keywords: Differential Categories, Integral Categories, Calculus Categories}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 2 2020
  • 2 2017

  • Refine by Author
  • 3 Cockett, Robin
  • 2 Lemay, Jean-Simon
  • 2 Lemay, Jean-Simon Pacaud
  • 1 Cockett, J. Robin B.
  • 1 Cruttwell, Geoffrey
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Categorical semantics
  • 2 Theory of computation → Linear logic
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Program semantics
  • Show More...

  • Refine by Keyword
  • 2 Coalgebra Modalities
  • 2 Differential Categories
  • 2 Linear Logic
  • 1 Automatic Differentiation
  • 1 Bialgebra Modalities
  • Show More...

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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact