Search Results

Documents authored by Damato, Stefania

Artifact
Software
DOI: 10.4230/artifacts.24710
stefaniatadama/formalising-inductive-coinductive-containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Abstract
Cite as

Stefania Damato, Thorsten Altenkirch, Axel Ljungström. stefaniatadama/formalising-inductive-coinductive-containers (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24710,
   title = {{stefaniatadama/formalising-inductive-coinductive-containers}}, 
   author = {Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4;origin=https://github.com/stefaniatadama/formalising-inductive-coinductive-containers;visit=swh:1:snp:eebf2acbd002c4877bc6057e65e8ddef2b0fe79e;anchor=swh:1:rev:4e587677bdc0c7cb793ad8612c1e6e88c16877e7}{\texttt{swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4}} (visited on 2025-09-22)},
   url = {https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda},
   doi = {10.4230/artifacts.24710},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.17
Formalising Inductive and Coinductive Containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-Löf type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that "containers preserve least and greatest fixed points" in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda’s path type to coinductive proofs.
Cite as

Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. Formalising Inductive and Coinductive Containers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{damato_et_al:LIPIcs.ITP.2025.17,
  author =	{Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
  title =	{{Formalising Inductive and Coinductive Containers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.17},
  URN =		{urn:nbn:de:0030-drops-246151},
  doi =		{10.4230/LIPIcs.ITP.2025.17},
  annote =	{Keywords: type theory, container, initial algebra, terminal coalgebra, Cubical Agda}
}
Artifact
Software
DOI: 10.4230/artifacts.24062
chrisjpurdy/distr-laws-of-monadic-containers

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24062,
   title = {{chrisjpurdy/distr-laws-of-monadic-containers}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a;origin=https://github.com/chrisjpurdy/distr-laws-of-monadic-containers;visit=swh:1:snp:053b593aa05da0a8be19fd62a74e2acaf9afad94;anchor=swh:1:rev:2c5f94536e8a52b98e3dc466b07511f106acb882}{\texttt{swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a}} (visited on 2025-07-28)},
   url = {https://github.com/chrisjpurdy/distr-laws-of-monadic-containers},
   doi = {10.4230/artifacts.24062},
}
Artifact
Software
DOI: 10.4230/artifacts.24064
chrisjpurdy/distr-laws-of-monadic-containers HTML rendering

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers HTML rendering (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24064,
   title = {{chrisjpurdy/distr-laws-of-monadic-containers HTML rendering}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software (visited on 2025-07-28)},
   url = {https://stefaniatadama.com/distr-law-mnd-cont-html/},
   doi = {10.4230/artifacts.24064},
}
Artifact
Software
DOI: 10.4230/artifacts.24065
stefaniatadama/cubical

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. stefaniatadama/cubical (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24065,
   title = {{stefaniatadama/cubical}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software (visited on 2025-07-28)},
   url = {https://github.com/stefaniatadama/cubical/tree/distr-laws},
   doi = {10.4230/artifacts.24065},
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.4
Distributive Laws of Monadic Containers

Authors: Chris Purdy and Stefania Damato

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose. In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu’s characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the "zoo" of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.
Cite as

Chris Purdy and Stefania Damato. Distributive Laws of Monadic Containers. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{purdy_et_al:LIPIcs.CALCO.2025.4,
  author =	{Purdy, Chris and Damato, Stefania},
  title =	{{Distributive Laws of Monadic Containers}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.4},
  URN =		{urn:nbn:de:0030-drops-235633},
  doi =		{10.4230/LIPIcs.CALCO.2025.4},
  annote =	{Keywords: distributive laws, monadic containers, monads, dependent types, cubical agda}
}
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