bsc-leon-vatthauer/slides/bibliography.bib

@article{delay,
  author     = {Venanzio Capretta},
  title      = {General Recursion via Coinductive Types},
  journal    = {CoRR},
  volume     = {abs/cs/0505037},
  year       = {2005},
  url        = {http://arxiv.org/abs/cs/0505037},
  eprinttype = {arXiv},
  eprint     = {cs/0505037},
  timestamp  = {Mon, 13 Aug 2018 16:46:14 +0200},
  biburl     = {https://dblp.org/rec/journals/corr/abs-cs-0505037.bib},
  bibsource  = {dblp computer science bibliography, https://dblp.org}
}

@article{elgotalgebras,
  author     = {Jir{\'{\i}} Ad{\'{a}}mek and
                Stefan Milius and
                Jir{\'{\i}} Velebil},
  title      = {Elgot Algebras},
  journal    = {CoRR},
  volume     = {abs/cs/0609040},
  year       = {2006},
  url        = {http://arxiv.org/abs/cs/0609040},
  eprinttype = {arXiv},
  eprint     = {cs/0609040},
  timestamp  = {Mon, 04 Sep 2023 12:29:24 +0200},
  biburl     = {https://dblp.org/rec/journals/corr/abs-cs-0609040.bib},
  bibsource  = {dblp computer science bibliography, https://dblp.org}
}

@article{elgotmonad,
  title     = {Elgot theories: a new perspective on the equational properties of iteration},
  volume    = {21},
  doi       = {10.1017/S0960129510000496},
  number    = {2},
  journal   = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  author    = {Jir{\'{\i}} Ad{\'{a}}mek and
               Stefan Milius and
               Jir{\'{\i}} Velebil},
  year      = {2011},
  pages     = {417–480}
}

@article{eqlm,
  author     = {Bucalo, Anna and F\"{u}hrmann, Carsten and Simpson, Alex},
  title      = {An Equational Notion of Lifting Monad},
  year       = {2003},
  issue_date = {15 February 2003},
  publisher  = {Elsevier Science Publishers Ltd.},
  address    = {GBR},
  volume     = {294},
  number     = {1–2},
  issn       = {0304-3975},
  url        = {https://doi.org/10.1016/S0304-3975(01)00243-2},
  doi        = {10.1016/S0304-3975(01)00243-2},
  abstract   = {We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring nonequational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.},
  journal    = {Theor. Comput. Sci.},
  month      = {2},
  pages      = {31–60},
  numpages   = {30},
  keywords   = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
}

@article{moggi,
  author     = {Moggi, Eugenio},
  title      = {Notions of Computation and Monads},
  year       = {1991},
  issue_date = {July 1991},
  publisher  = {Academic Press, Inc.},
  address    = {USA},
  volume     = {93},
  number     = {1},
  issn       = {0890-5401},
  url        = {https://doi.org/10.1016/0890-5401(91)90052-4},
  doi        = {10.1016/0890-5401(91)90052-4},
  journal    = {Inf. Comput.},
  month      = {7},
  pages      = {55–92},
  numpages   = {38}
}

@inproceedings{quotienting,
  author    = {Chapman, James and Uustalu, Tarmo and Veltri, Niccol\`{o}},
  title     = {Quotienting the Delay Monad by Weak Bisimilarity},
  year      = {2015},
  isbn      = {9783319251493},
  publisher = {Springer-Verlag},
  address   = {Berlin, Heidelberg},
  url       = {https://doi.org/10.1007/978-3-319-25150-9_8},
  doi       = {10.1007/978-3-319-25150-9_8},
  abstract  = {The delay datatype was introduced by Capretta [3] as a means to deal with partial functions as in computability theory in Martin-L\"{o}f type theory. It is a monad and it constitutes a constructive alternative to the maybe monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay monad quotiented by weak bisimilarity is still a monad. In this paper, we consider Hofmann's alternative approach [6] of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the semi-classical axiom of countable choice. We have fully formalized our results in the Agda dependently typed programming language.},
  booktitle = {Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 9399},
  pages     = {110–125},
  numpages  = {16}
}

@article{restriction,
  author     = {Cockett, J. R. B. and Lack, Stephen},
  title      = {Restriction Categories I: Categories of Partial Maps},
  year       = {2002},
  issue_date = {January},
  publisher  = {Elsevier Science Publishers Ltd.},
  address    = {GBR},
  volume     = {270},
  number     = {1–2},
  issn       = {0304-3975},
  url        = {https://doi.org/10.1016/S0304-3975(00)00382-0},
  doi        = {10.1016/S0304-3975(00)00382-0},
  abstract   = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
  journal    = {Theor. Comput. Sci.},
  month      = {1},
  pages      = {223–259},
  numpages   = {37}
}

@article{uniformelgot,
  author     = {Sergey Goncharov},
  title      = {Uniform Elgot Iteration in Foundations},
  journal    = {CoRR},
  volume     = {abs/2102.11828},
  year       = {2021},
  url        = {https://arxiv.org/abs/2102.11828},
  eprinttype = {arXiv},
  eprint     = {2102.11828},
  timestamp  = {Fri, 26 Feb 2021 14:31:25 +0100},
  biburl     = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
  bibsource  = {dblp computer science bibliography, https://dblp.org}
}

@article{while,
  author     = {Sergey Goncharov and
                Lutz Schr{\"{o}}der and
                Christoph Rauch},
  title      = {(Co-)Algebraic Foundations for Effect Handling and Iteration},
  journal    = {CoRR},
  volume     = {abs/1405.0854},
  year       = {2014},
  url        = {http://arxiv.org/abs/1405.0854},
  eprinttype = {arXiv},
  eprint     = {1405.0854},
  timestamp  = {Mon, 13 Aug 2018 16:47:19 +0200},
  biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
  bibsource  = {dblp computer science bibliography, https://dblp.org}
}