refs.bib

@book{aguiarMonoidalFunctorsSpecies2010,
  title = {Monoidal Functors, Species, and {{Hopf}} Algebras},
  author = {Aguiar, Marcelo and Mahajan, Swapneel Arvind},
  date = {2010},
  series = {{{CRM}} Monograph Series / {{Centre}} de Recherches Mathématiques, {{Montréal}}},
  number = {v. 29},
  publisher = {American Mathematical Society},
  location = {Providence, R.I},
  url = {http://pi.math.cornell.edu/~maguiar/a.pdf},
  isbn = {978-0-8218-4776-3},
  pagetotal = {784},
  keywords = {Categories (Mathematics),Combinatorial analysis,Hopf algebras,Quantum groups,Symmetry groups}
}

@article{arkorEnhanced2categoricalStructures,
  title = {Enhanced 2-Categorical Structures},
  author = {Arkor, Nathanael and Bourke, John and Ko, Joanna}
}

@article{bakovicFibrationsBicategories,
  title = {Fibrations of Bicategories},
  author = {Baković, Igor},
  abstract = {he main purpose of this work is to describe a generalization of the Grothendieck construction for pseudofunctors which provides a biequivalence between the 2-categories of pseudofunctors and fibrations. For any bicategory B, we describe a tricategory of B- indexeded bicategories which are the weakest possible generalization of pseudofunctors to the immediate next level. Then we introduce a notion of a fibration of bicategories, which generalizes 2-fibrations of strict 2-categories defined by Hermida. Finally we give an explicit construction of an analog of the Grothendieck construction which provides a triequivalence between the 3-category of B-indexeded bicategories and the 3-category of 2-fibrations over B.}
}

@online{bakovicGrothendieckConstructionBicategories,
  title = {Grothendieck Construction for Bicategories},
  author = {Baković, Igor},
  location = {Rudjer Bošković Institute},
  url = {https://www2.irb.hr/korisnici/ibakovic/sgc.pdf},
  abstract = {In this article, we give the generalization of the Grothendieck construction for pseudo functors given in [5], which provides a biequivalence between the 2-categories of pseudofunctors and fibrations. We define the second Grothendieck construction which to any pseudo 2-functor associates a 2-fibration, defined by Hermida [6], and we prove the biequivalence between the 2-category of pseudo 2-functors and the 2-category of 2-fibrations.},
  langid = {english},
  pubstate = {prepublished}
}

@incollection{barrAcyclicModelsTriples1966,
  title = {Acyclic {{Models}} and {{Triples}}},
  booktitle = {Proceedings of the {{Conference}} on {{Categorical Algebra}}},
  author = {Barr, Michael and Beck, Jon},
  editor = {Eilenberg, S. and Harrison, D. K. and MacLane, S. and Röhrl, H.},
  date = {1966},
  pages = {336--343},
  publisher = {Springer Berlin Heidelberg},
  location = {Berlin, Heidelberg},
  doi = {10.1007/978-3-642-99902-4_16},
  url = {http://link.springer.com/10.1007/978-3-642-99902-4_16},
  urldate = {2023-02-19},
  isbn = {978-3-642-99904-8},
  langid = {english}
}

@article{barrCartanEilenbergCohomologyTriples1996,
  title = {Cartan-{{Eilenberg}} Cohomology and Triples},
  author = {Barr, Michael},
  date = {1996-11},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {112},
  number = {3},
  pages = {219--238},
  issn = {00224049},
  doi = {10.1016/0022-4049(95)00138-7},
  url = {https://linkinghub.elsevier.com/retrieve/pii/0022404995001387},
  urldate = {2023-02-19},
  langid = {english},
  file = {/home/patrick/Zotero/storage/MPHYTJVF/Barr - 1996 - Cartan-Eilenberg cohomology and triples.pdf}
}

@inproceedings{barrCompositeCotriplesDerived1966,
  title = {Composite {{Cotriples}} and {{Derived Functors}}},
  booktitle = {Seminar on {{Triples}} and {{Categorical Homology Theory}}},
  author = {Barr, Michael},
  date = {1966/1967},
  volume = {80},
  pages = {336},
  publisher = {Springer-Verlag},
  location = {Forschungsinstitut fur MathematiK, ETH, Zurich.},
  abstract = {The main result of [2] is that the cohomology of an algebra with respect to the free associative algebra cotriple can be described by the resolution given by U. Shukla in [8]. That looks like a composite resolution; first an algebra is  resolved by means of free modules (over the ground ring) and then this resolution is given the structure of a DG-algebra and resolved by the categorical bar resolution. This suggests that similar results might be obtained for all categories of objects with "two structures". Not surprisingly this turns out to involve a coherence condition between the structures which,for ordinary algebras, turns out to reduce to the  distributive law. It was suggested in this connection by J. Beck and H. Appelgate.},
  eventtitle = {Seminar on {{Triples}} and {{Categorical Homology Theory}}},
  isbn = {978-3-540-04601-1},
  langid = {english}
}

@article{barrContractibleSimplicialObjects2019,
  title = {Contractible Simplicial Objects},
  author = {Barr, Michael and Kennison, John F. and Raphael, Robert M.},
  date = {2019},
  journaltitle = {Commentationes Mathematicae Universitatis Carolinae},
  volume = {60},
  number = {4},
  pages = {473--495},
  publisher = {{Charles University in Prague, Faculty of Mathematics and Physics}},
  issn = {0010-2628},
  url = {https://eudml.org/doc/295068},
  urldate = {2022-12-23},
  langid = {english},
  file = {/home/patrick/Zotero/storage/RG3PKWIX/295068.html}
}

@article{barrContractibleSimplicialObjects2020,
  title = {Contractible Simplicial Objects},
  author = {Barr, Michael and Kennison, John F. and Raphael, Robert},
  date = {2020-02-21},
  journaltitle = {Commentationes Mathematicae Universitatis Carolinae},
  volume = {60},
  number = {4},
  pages = {473--495},
  issn = {0010-2628, 1213-7243},
  doi = {10.14712/1213-7243.2019.023},
  url = {http://cmuc.karlin.mff.cuni.cz/doi/10.14712/1213-7243.2019.023},
  urldate = {2022-12-23},
  abstract = {We raise the question of when a simplicial object in a category is deemed contractible. The literature offers three definitions. One is the existence of an “extra degeneracy”, indexed by −1, which does not quite live up to the name. This can be strengthened to a “strong extra degeneracy”. Another possibility is that it be homotopic to a constant simplicial object. Despite claims in the literature to the contrary, we show that all three are distinct concepts with strong extra degeneracy implies extra degeneracy implies homotopic to a constant and give explicit examples to show the converses fail.},
  langid = {english},
  file = {/home/patrick/Zotero/storage/K33DI7SC/Michael et al. - 2020 - Contractible simplicial objects.pdf}
}

@inproceedings{barrHomologyStandardConstructions1966,
  title = {Homology and {{Standard Constructions}}},
  booktitle = {Seminar on {{Triples}} and {{Categorical Homology Theory}}},
  author = {Barr, Michael and Beck, Jonathan},
  date = {1966/1967},
  series = {Forschungsinstitut Fur {{Mathematik}}, {{ETH}}, {{Zurich}}},
  volume = {80},
  pages = {245--345},
  publisher = {Springer-Verlag},
  location = {Forschungsinstitut fur Mathematik, ETH, Zurich.},
  abstract = {In ordinary homological algebra, if M is an R-module, the usual way of starting to construct a projective resolution of M is to let F be the free R-module generated by the elements of M and F -* M the epimorphism determined by (m) -+ m . One then takes the kernel of F -* M and continues the process. But notice that in the construction of F -+ M a lot of structure is customarily overlooked. F is actually a functor MG of M , F -+ M is an instance of a natural transformation G -+ (identity functor) ; there is also a "comultiplication" G -+ GG which is a little less evident. The functor G , equipped with these structures, is an example of what is called a standard construction or "cotriple". In this paper we start with a category C, , a cotriple 6 in C. , and show how resolutions and derived functors or homology can be constructed by means of this tool alone. The category C. will be non-abelian in general (note that even for modules the cotriple employed fails to respect the additive structure of the category), and the coefficients will consist of an arbitrary functor E : C. -+ Q. where \& is an abelian category. For ordinary homology and cohomology theories, E will be tensoring, homming or deriving with or into a module of some kind. To summarize the contents of the paper: In § 1 we define the derived functors and give several examples of categories with cotriples. In § 2 we study the derived functors H ( »E)\textasciicircum{} as functors on C, and give several of their properties. In § 3 we fix a first variable X e C. and study H (X, ) as a functor of the abelian variable E . As such it admits a simple axiomatic characterization. § 4 considers the case in which C. is additive and shows that the general theory can always, in effect, be reduced to that case. In § 5 we study the relation between cotriples and projective classes (defined - essentially - by Eilenberg-Moore [ 16 ]) and show that the  homology only depends on the projective class defined by the cotriple. §§ 6-9 are concerned largely with various special properties that these derived functors possess in well known algebraic categories (groups, modules, algebras, ....). In § 10 we consider the problem of defining a cotriple to produce a given projective class (in a sense, the converse problem to that studied in § 5) by means of "models". We also compare the results with other theories of derived functors based on models. § 11 is concerned with some technical items on acyclic models.},
  langid = {english}
}

@article{barthelConstructionFunctorialFactorizations2013,
  title = {On the Construction of Functorial Factorizations for Model Categories},
  author = {Barthel, Tobias and Riehl, Emily},
  date = {2013-04-17},
  journaltitle = {Algebraic \& Geometric Topology},
  shortjournal = {Algebr. Geom. Topol.},
  volume = {13},
  number = {2},
  eprint = {1204.5427},
  eprinttype = {arXiv},
  eprintclass = {math},
  pages = {1089--1124},
  issn = {1472-2739, 1472-2747},
  doi = {10.2140/agt.2013.13.1089},
  url = {http://arxiv.org/abs/1204.5427},
  urldate = {2023-01-03},
  abstract = {We present general techniques for constructing functorial factorizations appropriate for model structures that are not known to be cofibrantly generated. Our methods use "algebraic" characterizations of fibrations to produce factorizations that have the desired lifting properties in a completely categorical fashion. We illustrate these methods in the case of categories enriched, tensored, and cotensored in spaces, proving the existence of Hurewicz-type model structures, thereby correcting an error in earlier attempts by others. Examples include the categories of (based) spaces, (based) G-spaces, and diagram spectra among others.},
  keywords = {55U35 55U40 18A32 18G55,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  note = {Comment: Final journal version to appear in Algebraic \& Geometric Topology with improvements suggested by the referee},
  file = {/home/patrick/Zotero/storage/R3VZX9GE/On the construction of functori - Emily Riehl.pdf}
}

@online{barthelSixModelStructures2014,
  title = {Six Model Structures for {{DG-modules}} over {{DGAs}}: {{Model}} Category Theory in Homological Action},
  shorttitle = {Six Model Structures for {{DG-modules}} over {{DGAs}}},
  author = {Barthel, Tobias and May, J. P. and Riehl, Emily},
  date = {2014-08-03},
  eprint = {1310.1159},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1310.1159},
  urldate = {2023-01-03},
  abstract = {In Part 1, we describe six projective-type model structures on the category of differential graded modules over a differential graded algebra A over a commutative ring R. When R is a field, the six collapse to three and are well-known, at least to folklore, but in the general case the new relative and mixed model structures offer interesting alternatives to the model structures in common use. The construction of some of these model structures requires two new variants of the small object argument, an enriched and an algebraic one, and we describe these more generally. In Part 2, we present a variety of theoretical and calculational cofibrant approximations in these model categories. The classical bar construction gives cofibrant approximations in the relative model structure, but generally not in the usual one. In the usual model structure, there are two quite different ways to lift cofibrant approximations from the level of homology modules over homology algebras, where they are classical projective resolutions, to the level of DG-modules over DG-algebras. The new theory makes model theoretic sense of earlier explicit calculations based on one of these constructions. A novel phenomenon we encounter is isomorphic cofibrant approximations with different combinatorial structure such that things proven in one avatar are not readily proven in the other.},
  pubstate = {prepublished},
  keywords = {16E45 18G25 18G55 55S30 55T20 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - K-Theory and Homology},
  note = {Comment: 68 pages; v2: various expositional improvements suggested by an anonymous referee},
  file = {/home/patrick/Zotero/storage/GCLU3IQN/Barthel et al. - 2014 - Six model structures for DG-modules over DGAs Mod.pdf;/home/patrick/Zotero/storage/W8ULC6NZ/1310.html}
}

@inproceedings{beckDistributiveLaws1966,
  title = {Distributive {{Laws}}},
  booktitle = {Seminar on {{Triples}} and {{Categorical Homology Theory}}},
  author = {Beck, Jonathan},
  date = {1966/1967},
  volume = {80},
  pages = {119--140},
  publisher = {Springer-Verlag},
  location = {Forschungsinstitut fur MathematiK, ETH, Zurich.},
  abstract = {The usual distributive law of multiplication over addition, (x + x..) (y +y, )-* x y + xy + x y + x y , combines the mathematical structures of abelian groups and monoids to produce the more interesting and complex structure of rings. From the point of view of "triples," a distributive law provides a way of interchanging two types of operations and making the functorial composition of two triples into a more complex triple. The main formal properties and different ways of looking at distributive laws are given in §1. §2 is about algebras over composite triples. These are found to be objects with two structures, and the distributive law or interchange of operations appears in its usual form as an equation which the two types of operations must obey. §3 is about some frequently-occurring diagrams of adjoint functors which are connected with distributive laws. §4 is devoted to Examples. There is an Appendix on compositions of adjoint functors.},
  eventtitle = {Seminar on {{Triples}} and {{Categorical Homology Theory}}},
  isbn = {978-3-540-04601-1},
  langid = {english}
}

@thesis{beckTriplesAlgebrasCohomology1967,
  title = {Triples, {{Algebras}} and {{Cohomology}}},
  author = {Beck, Jonathan},
  date = {1967},
  institution = {Columbia University},
  url = {http://www.tac.mta.ca/tac/reprints/articles/2/tr2.pdf},
  urldate = {2023-02-19},
  abstract = {This thesis is intended to complete the exposition in [Eilenberg \& Moore (1965a)] with regard to certain points. In §1 we recall the definitions of triple, algebra over a triple, and give our main (original) definition, that of tripleable adjoint pair of functors. In §2 we show how to obtain a cohomology theory from an adjoint pair of functors. In §3, when the adjoint pair is tripleable, we prove that the cohomology group H1 classifies principal homogeneous objects. When coefficients are in a module, principal objects are interpreted as algebra extensions. §4 is devoted to examples. Many categories occurring in algebra are shown to be tripleable. The corresponding cohomology and extension theories, ranging from groups and algebras to the classical Ext(A, C), are discussed. Many new theories arise. A method for proving coincidence of triple cohomology with certain standard theories has been given by [Barr \& Beck (1966)]. That paper contains a summary of the present work.},
  langid = {english},
  pagetotal = {60}
}

@book{bibelConferenceAutomatedDeduction1980,
  title = {Conference on {{Automated Deduction}}. 5: {{Les Arcs}}, {{France}}, {{July}} 8 - 11, 1980 / Ed. by {{W}}. {{Bibel}}},
  shorttitle = {Conference on {{Automated Deduction}}. 5},
  editor = {Bibel, Wolfgang},
  date = {1980},
  series = {Lecture Notes in Computer Science},
  number = {87},
  eventtitle = {Conference on {{Automated Deduction}}},
  isbn = {978-3-540-10009-6 978-0-387-10009-8},
  langid = {english},
  pagetotal = {385}
}

@article{bourkeAlgebraicWeakFactorisation2016,
  title = {Algebraic Weak Factorisation Systems {{II}}: {{Categories}} of Weak Maps},
  shorttitle = {Algebraic Weak Factorisation Systems {{II}}},
  author = {Bourke, John and Garner, Richard},
  date = {2016-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {220},
  number = {1},
  pages = {148--174},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2015.06.003},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0022404915001711},
  urldate = {2023-05-29},
  langid = {english},
  file = {/home/patrick/Zotero/storage/3TS7Z366/Bourke and Garner - 2016 - Algebraic weak factorisation systems II Categorie.pdf}
}

@article{bourkeAlgebraicWeakFactorisation2016a,
  title = {Algebraic Weak Factorisation Systems {{I}}: {{Accessible AWFS}}},
  shorttitle = {Algebraic Weak Factorisation Systems {{I}}},
  author = {Bourke, John and Garner, Richard},
  date = {2016-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {220},
  number = {1},
  pages = {108--147},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2015.06.002},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S002240491500170X},
  urldate = {2023-05-29},
  langid = {english},
  file = {/home/patrick/Zotero/storage/MEM4IY5Q/Bourke and Garner - 2016 - Algebraic weak factorisation systems I Accessible.pdf}
}

@online{brandenburgTensorCategoricalFoundations2014,
  title = {Tensor Categorical Foundations of Algebraic Geometry},
  author = {Brandenburg, Martin},
  date = {2014-10-07},
  eprint = {1410.1716},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1410.1716},
  urldate = {2023-02-04},
  abstract = {Tannaka duality and its extensions by Lurie, Sch¨appi et al. reveal that many schemes as well as algebraic stacks may be identified with their tensor categories of quasi-coherent sheaves. In this thesis we study constructions of cocomplete tensor categories (resp. cocontinuous tensor functors) which usually correspond to constructions of schemes (resp. their morphisms) in the case of quasi-coherent sheaves. This means to globalize the usual local-global algebraic geometry. For this we first have to develop basic commutative algebra in an arbitrary cocomplete tensor category. We then discuss tensor categorical globalizations of affine morphisms, projective morphisms, immersions, classical projective embeddings (Segre, Plu¨cker, Veronese), blow-ups, fiber products, classifying stacks and finally tangent bundles. It turns out that the universal properties of several moduli spaces or stacks translate to the corresponding tensor categories.},
  langid = {english},
  pubstate = {prepublished},
  keywords = {Mathematics - Algebraic Geometry,Mathematics - Category Theory},
  note = {Comment: PhD thesis; 247 pages},
  file = {/home/patrick/Zotero/storage/N49MNC2Z/Brandenburg - 2014 - Tensor categorical foundations of algebraic geomet.pdf}
}

@online{buckleyFibred2categoriesBicategories2013,
  title = {Fibred 2-Categories and Bicategories},
  author = {Buckley, Mitchell},
  date = {2013-03-25},
  eprint = {1212.6283},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.48550/arXiv.1212.6283},
  url = {http://arxiv.org/abs/1212.6283},
  urldate = {2025-11-29},
  abstract = {We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond to trihomomorphisms from a bicategory into Bicat. We describe the Grothendieck construction for each kind of fibration and present a few examples of each. Fibrations in our sense, between bicategories, are closed under composition and are stable under equiv-comma. The free such fibration on a homomorphism is obtained by taking an oplax comma along an identity.},
  pubstate = {prepublished},
  keywords = {Mathematics - Category Theory},
  note = {Comment: Changes to the introduction: gives a better description of how our work relates to the work of others. Added a few remarks},
  file = {/home/patrick/Zotero/storage/N68IZ5ER/Buckley - 2013 - Fibred 2-categories and bicategories.pdf;/home/patrick/Zotero/storage/WNL4UPCR/1212.html}
}

@article{buckleyFibred2categoriesBicategories2014,
  title = {Fibred 2-Categories and Bicategories},
  author = {Buckley, Mitchell},
  date = {2014-06},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {218},
  number = {6},
  pages = {1034--1074},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2013.11.002},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0022404913002065},
  urldate = {2023-10-07},
  langid = {english},
  keywords = {2-category,bicategory,fibration},
  file = {/home/patrick/Zotero/storage/NDE3CWPT/Buckley - 2014 - Fibred 2-categories and bicategories.pdf}
}

@article{carboniConnectedLimitsFamilial1995,
  title = {Connected Limits, Familial Representability and {{Artin}} Glueing},
  author = {Carboni, Aurelio and Johnstone, Peter},
  date = {1995-12},
  journaltitle = {Mathematical Structures in Computer Science},
  shortjournal = {Math. Struct. Comp. Sci.},
  volume = {5},
  number = {4},
  pages = {441--459},
  issn = {0960-1295, 1469-8072},
  doi = {10.1017/S0960129500001183},
  url = {https://www.cambridge.org/core/product/identifier/S0960129500001183/type/journal_article},
  urldate = {2023-02-20},
  abstract = {We consider the following two properties of a functor               F               from a presheaf topos to the category of sets: (a)               F               preserves connected limits, and (b) the Artin glueing of               F               is again a presheaf topos. We show that these two properties are in fact equivalent. In the process, we develop a general technique for associating categorical properties of a category obtained by Artin glueing with preservation properties of the functor along which the glueing takes place. We also give a syntactic characterization of those monads on Set whose functor parts have the above properties, and whose units and multiplications are cartesian natural transformations.},
  langid = {english}
}

@inproceedings{coenELPIFastEmbeddable2015,
  title = {{{ELPI}}: Fast, {{Embeddable}}, {{λProlog Interpreter}}},
  booktitle = {Proceedings of {{LPAR}}},
  author = {Coen, Claudio Sacerdoti and Tassi, Enrico and Dunchev, Cvetan and Guidi, Ferrucio},
  date = {2015-11},
  location = {Suva, Fiji},
  abstract = {We present a new interpreter for λProlog that runs consistently faster than the byte code compiled by Teyjus, that is believed to be the best available implementation of λProlog. The key insight is the identification of a fragment of the language, which we call reduction-free fragment (L β λ), that occurs quite naturally in λProlog programs and that admits constant time reduction and unification rules.},
  eventtitle = {Logic for {{Programming}}, {{Artificial Intelligence}} and {{Reasoning}}}
}

@article{cruttwellDoubleFibrations2022,
  title = {Double {{Fibrations}}},
  author = {Cruttwell, G. S. H. and Lambert, M. J. and Pronk, D. A. and Szyld, M},
  date = {2022},
  journaltitle = {Theory and Applications of Categories},
  shortjournal = {T.A.C.},
  volume = {38},
  number = {35},
  pages = {1326--1394},
  url = {http://www.tac.mta.ca/tac/volumes/38/35/38-35abs.html},
  langid = {english}
}

@article{cruttwellUnifiedFrameworkGeneralized2010,
  title = {A Unified Framework for Generalized Multicategories},
  author = {Cruttwell, G. S. H. and Shulman, Michael A.},
  date = {2010-04-05},
  journaltitle = {Theory and Applications of Categories},
  shortjournal = {Theory appl. categ.},
  volume = {24},
  number = {21},
  pages = {580--655},
  issn = {1201-561X},
  url = {http://www.tac.mta.ca/tac/volumes/24/21/24-21.pdf},
  abstract = {Notions of generalized multicategory have been defined in numerous con- texts throughout the literature, and include such diverse examples as symmetric multi- categories, globular operads, Lawvere theories, and topological spaces. In each case, generalized multicategories are defined as the “lax algebras” or “Kleisli monoids” rela- tive to a “monad” on a bicategory. However, the meanings of these words differ from author to author, as do the specific bicategories considered. We propose a unified frame- work: by working with monads on double categories and related structures (rather than bicategories), one can define generalized multicategories in a way that unifies all previous examples, while at the same time simplifying and clarifying much of the theory.}
}

@article{dawsonSpanConstruction2010,
  title = {The {{Span Construction}}},
  author = {Dawson, Robert and Pronk, Dorette and Paré, Robert},
  date = {2010},
  journaltitle = {Theory and Applications of Categories},
  volume = {24},
  number = {13},
  pages = {302--377}
}

@article{doldPartitionsUnityTheory1963,
  title = {Partitions of {{Unity}} in the {{Theory}} of {{Fibrations}}},
  author = {Dold, Albrecht},
  date = {1963-09},
  journaltitle = {The Annals of Mathematics},
  shortjournal = {The Annals of Mathematics},
  volume = {78},
  number = {2},
  eprint = {1970341},
  eprinttype = {jstor},
  pages = {223},
  issn = {0003486X},
  doi = {10.2307/1970341},
  url = {https://www.jstor.org/stable/1970341?origin=crossref},
  urldate = {2023-05-27}
}

@article{dumancicKnowledgeRefactoringInductive2021,
  title = {Knowledge {{Refactoring}} for {{Inductive Program Synthesis}}},
  author = {Dumancic, Sebastijan and Guns, Tias and Cropper, Andrew},
  date = {2021-05-18},
  journaltitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
  shortjournal = {AAAI},
  volume = {35},
  number = {8},
  pages = {7271--7278},
  issn = {2374-3468, 2159-5399},
  doi = {10.1609/aaai.v35i8.16893},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/16893},
  urldate = {2023-04-24},
  abstract = {Humans constantly restructure knowledge to use it more efficiently. Our goal is to give a machine learning system similar abilities so that it can learn more efficiently. We introduce the knowledge refactoring problem, where the goal is to restructure a learner's knowledge base to reduce its size and to minimise redundancy in it. We focus on inductive logic programming, where the knowledge base is a logic program. We introduce Knorf, a system which solves the refactoring problem using constraint optimisation. A key feature of Knorf is that, rather than simply removing knowledge, it also introduces new knowledge through predicate invention. We evaluate our approach on two domains: building Lego structures and real-world string transformations. Our experiments show that learning from refactored knowledge can improve predictive accuracies fourfold and reduce learning times by half.},
  file = {/home/patrick/Zotero/storage/9LQNLD7M/Dumancic et al. - 2021 - Knowledge Refactoring for Inductive Program Synthe.pdf}
}

@thesis{duncanUseDataMiningAutomatic2007,
  title = {The {{Use}} of {{Data-Mining}} for the {{Automatic Formation}} of {{Tactics}}},
  author = {Duncan, Hazel},
  date = {2007},
  institution = {School of Informatics, University of Edinburgh},
  location = {UK},
  url = {http://gpbib.cs.ucl.ac.uk/gp-html/hazelthesis.html},
  abstract = {As functions which further the state of a proof in automated theorem proving, tactics are an important development in automated deduction. This thesis describes a method to tackle the problem of tactic formation. Tactics must currently be developed by hand, which can be a complicated and time-consuming process. A method is presented for the automatic production of useful tactics. The method presented works on the principle that commonly occurring patterns within proof corpora may have some significance and could therefore be exploited to provide novel tactics. These tactics are discovered using a three step process. Firstly a suitable corpus is chosen and processed. One example of a suitable corpus is that of the Isabelle theorem prover. A number of possible abstractions are presented for this corpus. Secondly, machine learning techniques are used to data-mine each corpus and find sequences of commonly occurring proof steps. The specifics of a proof step are defined by the specified abstraction. The formation of these tactics is completed using evolutionary techniques to combine these patterns into compound tactics. These new tactics are applied using a naive prover as well as undergoing manual evaluation. The tactics show favourable results across a selection of tests, justifying the claim that this project provides a novel method of automatically producing tactics which are both viable and useful},
  langid = {english},
  pagetotal = {151}
}

@incollection{dwyerHomotopyTheoriesModel,
  title = {Homotopy Theories and Model Categories},
  booktitle = {Handbook of {{Algebraic Topology}}},
  author = {Dwyer, William G. and Spalinski, J.},
  publisher = {Elsevier},
  isbn = {978-0-444-81779-2}
}

@incollection{dwyerHomotopyTheoriesModel1995,
  title = {Homotopy Theories and Model Categories},
  booktitle = {Handbook of Algebraic Topology},
  author = {Dwyer, William G. and Spalinski, J.},
  editor = {James, I. M.},
  date = {1995},
  publisher = {Elsevier Science B.V},
  location = {Amsterdam ; New York},
  url = {https://math.jhu.edu/~eriehl/616-s16/DwyerSpalinski.pdf},
  abstract = {This paper is an introduction to the theory of “model categories”, which was devel- oped by Quillen in [22] and [23]. By definition a model category is just an ordinary category with three specified classes of morphisms, called fibrations, cofibrations and weak equivalences, which satisfy a few simple axioms that are deliberately rem- iniscent of properties of topological spaces. Surprisingly enough, these axioms give a reasonably general context in which it is possible to set up the basic machinery of homotopy theory. The machinery can then be used immediately in a large number of different settings, as long as the axioms are checked in each case. Although many of these settings are geometric (spaces (§8), fibrewise spaces (3.11), G-spaces [11], spectra [5], diagrams of spaces [10] . . .), some of them are not (chain complexes (§7), simplicial commutative rings [24], simplicial groups [23] . . .). Certainly each setting has its own technical and computational peculiarities, but the advantage of an abstract approach is that they can all be studied with the same tools and described in the same language. What is the suspension of an augmented commuta- tive algebra? One of incidental appeals of Quillen’s theory (to a topologist!) is that it both makes a question like this respectable and gives it an interesting answer (11.3). We have tried to minimize the prerequisites needed for understanding this pa- per; it should be enough to have some familiarity with CW-complexes, with chain complexes, and with the basic terminology associated with categories. Almost all of the material we present is due to Quillen [22], but we have replaced his treatment of suspension functors and loop functors by a general construction of homotopy pushouts and homotopy pullbacks in a model category. What we do along these lines can certainly be carried further. This paper is not in any sense a survey of everything that is known about model categories; in fact we cover only a fraction of the material in [22]. The last section has a discussion of some ways in which model categories have been used in topology and algebra.},
  isbn = {978-0-444-81779-2},
  keywords = {Algebraic topology},
  file = {/home/patrick/Zotero/storage/XSRQQZ2S/Homotopy theories and model categories - W. G. Dwyer.pdf}
}

@inproceedings{ellisBiasReformulationOneShot2014,
  title = {Bias {{Reformulation}} for {{One-Shot Function Induction}}},
  booktitle = {Frontiers in {{Artificial Intelligence}} and {{Applications}}},
  author = {Ellis, Kevin and Lin, Dianhuan and Dechter, Eyal and Tenenbaum, Joshua B. and Muggleton, Stephen H.},
  date = {2014},
  pages = {7},
  publisher = {IOS Press},
  doi = {10.3233/978-1-61499-419-0-525},
  url = {https://dspace.mit.edu/handle/1721.1/102524},
  abstract = {In recent years predicate invention has been underexplored as a bias reformulation mechanism within Inductive Logic Programming due to difficulties in formulating efficient search mechanisms. However, recent papers on a new approach called Meta-Interpretive Learning have demonstrated that both predicate invention and learning recursive predicates can be efficiently implemented for various fragments of definite clause logic using a form of abduction within a meta-interpreter. This paper explores the effect of bias reformulation produced by Meta-Interpretive Learning on a series of Program Induction tasks involving string transformations. These tasks have real-world applications in the use of spreadsheet technology. The existing implementation of program induction in Microsoft’s FlashFill (part of Excel 2013) already has strong performance on this problem, and performs one-shot learning, in which a simple transformation program is generated from a single example instance and applied to the remainder of the column in a spreadsheet. However, no existing technique has been demonstrated to improve learning performance over a series of tasks in the way humans do. In this paper we show how a functional variant of the recently developed MetagolD system can be applied to this task. In experiments we study a regime of layered bias reformulation in which size-bounds of hypotheses are successively relaxed in each layer and learned programs re-use invented predicates from previous layers. Results indicate that this approach leads to consistent speed increases in learning, more compact definitions and consistently higher predictive accuracy over successive layers. Comparison to both FlashFill and human performance indicates that the new system, MetagolDF , has performance approaching the skill level of both an existing commercial system and that of humans on one-shot learning over the same tasks. The induced programs are relatively easily read and understood by a human programmer.},
  eventtitle = {Frontiers in {{Artificial Intelligence}} and {{Applications}}},
  isbn = {978-1-61499-419-0-525}
}

@online{ellisDreamCoderGrowingGeneralizable2020,
  title = {{{DreamCoder}}: {{Growing}} Generalizable, Interpretable Knowledge with Wake-Sleep {{Bayesian}} Program Learning},
  shorttitle = {{{DreamCoder}}},
  author = {Ellis, Kevin and Wong, Catherine and Nye, Maxwell and Sable-Meyer, Mathias and Cary, Luc and Morales, Lucas and Hewitt, Luke and Solar-Lezama, Armando and Tenenbaum, Joshua B.},
  date = {2020-06-15},
  eprint = {2006.08381},
  eprinttype = {arXiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/2006.08381},
  urldate = {2023-04-23},
  abstract = {Expert problem-solving is driven by powerful languages for thinking about problems and their solutions. Acquiring expertise means learning these languages -- systems of concepts, alongside the skills to use them. We present DreamCoder, a system that learns to solve problems by writing programs. It builds expertise by creating programming languages for expressing domain concepts, together with neural networks to guide the search for programs within these languages. A ``wake-sleep'' learning algorithm alternately extends the language with new symbolic abstractions and trains the neural network on imagined and replayed problems. DreamCoder solves both classic inductive programming tasks and creative tasks such as drawing pictures and building scenes. It rediscovers the basics of modern functional programming, vector algebra and classical physics, including Newton's and Coulomb's laws. Concepts are built compositionally from those learned earlier, yielding multi-layered symbolic representations that are interpretable and transferrable to new tasks, while still growing scalably and flexibly with experience.},
  pubstate = {prepublished},
  keywords = {Computer Science - Artificial Intelligence,Computer Science - Machine Learning},
  file = {/home/patrick/Zotero/storage/NXVGGDFM/Ellis et al. - 2020 - DreamCoder Growing generalizable, interpretable k.pdf;/home/patrick/Zotero/storage/76GXZ3X9/2006.html}
}

@thesis{farquharMetainterpretiveLearningProof2022,
  title = {Meta-Interpretive Learning of Proof Strategies},
  author = {Farquhar, Colin},
  date = {2022-05},
  institution = {Heriot-Watt University},
  location = {Edinburgh, Scotland},
  url = {https://www.ros.hw.ac.uk/handle/10399/4706},
  urldate = {2023-03-28},
  abstract = {In modern mathematics, mechanised theorem proving software is playing an ever increasing role. By enlisting the help of computers mathematicians are able to formally prove more complex results than they perhaps otherwise could, however those computers are still incapable of drawing many of the conclusions which would be obvious to a human user and so human intervention is still required. In this thesis we consider the use of an adapted machine learning technique to begin addressing this issue. We consider the use of proof strategies to provide a high-level view of how a proof is structured, including information about why a particular step was taken. We extend the Metagol meta-interpretive learning tool to facilitate learning these strategies. We begin with a small set of examples and refine our approach, demonstrating the improvements experimentally. We go on to discuss the learning of more complicated strategies, some of the issues faced in doing so and how we could address them. We conclude by evaluating the experiments as a whole, identifying the weak points in our approach and suggesting ways in which they can be addressed in future work.},
  langid = {english},
  pagetotal = {147}
}

@inproceedings{freitasVerifyingHeapAI4FM,
  title = {Verifying the Heap: An {{AI4FM}} Case Study},
  booktitle = {Contributions to \{{{AI4FM}}\} 2013},
  author = {Freitas, Leo and Jones, Cliff and Velykis, Andrius and Whiteside, Iain},
  series = {Technical {{Report}}, {{Heriot-Watt University}}},
  pages = {7--9},
  url = {http://www.macs.hw.ac.uk/cs/techreps/docs/files/HW-MACS-TR-0100.pdf},
  eventtitle = {{{ITP-WS-13}}}
}

@article{gambinoPolynomialFunctorsPolynomial2013,
  title = {Polynomial Functors and Polynomial Monads},
  author = {Gambino, Nicola and Kock, Joachim},
  date = {2013-01},
  journaltitle = {Mathematical Proceedings of the Cambridge Philosophical Society},
  shortjournal = {Math. Proc. Camb. Phil. Soc.},
  volume = {154},
  number = {1},
  pages = {153--192},
  issn = {0305-0041, 1469-8064},
  doi = {10.1017/S0305004112000394},
  url = {https://www.cambridge.org/core/product/identifier/S0305004112000394/type/journal_article},
  urldate = {2023-02-13},
  abstract = {Abstract             We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.},
  langid = {english},
  file = {/home/patrick/Zotero/storage/Q6TX4HPK/Gambino and Kock - 2013 - Polynomial functors and polynomial monads.pdf}
}

@online{garnerCofibrantlyGeneratedNatural2007,
  title = {Cofibrantly Generated Natural Weak Factorisation Systems},
  author = {Garner, Richard},
  date = {2007-02-12},
  eprint = {math/0702290},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/math/0702290},
  urldate = {2023-01-03},
  abstract = {There is an “algebraisation” of the notion of weak factorisation system (w.f.s.) known as a natural weak factorisation system. In it, the two classes of maps of a w.f.s. are replaced by two categories of maps-with-structure, where the extra structure on a map now encodes a choice of liftings with respect to the other class. This extra structure has pleasant consequences: for example, a natural w.f.s. on C induces a canonical natural w.f.s. structure on any functor category [A, C]. In this paper, we define cofibrantly generated natural weak factorisation systems by analogy with cofibrantly generated w.f.s.’s. We then construct them by a method which is reminiscent of Quillen’s small object argument but produces factorisations which are much smaller and easier to handle, and show that the resultant natural w.f.s. is, in a suitable sense, freely generated by its generating cofibrations. Finally, we show that the two categories of maps-with-structure for a natural w.f.s. are closed under all the constructions we would expect of them: (co)limits, pushouts / pullbacks, transfinite composition, and so on.},
  langid = {english},
  pubstate = {prepublished},
  keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  note = {Comment: 57 pages},
  file = {C:\Users\gadge\Documents\Books and Papers\Algebraic Topology and Homological Algebra\Cofibrantly Generated Weak Natural Factorization Systems - Garner.pdf}
}

@article{garnerUnderstandingSmallObject2009,
  title = {Understanding the Small Object Argument},
  author = {Garner, Richard},
  date = {2009-06},
  journaltitle = {Applied Categorical Structures},
  shortjournal = {Appl Categor Struct},
  volume = {17},
  number = {3},
  eprint = {0712.0724},
  eprinttype = {arXiv},
  eprintclass = {math},
  pages = {247--285},
  issn = {0927-2852, 1572-9095},
  doi = {10.1007/s10485-008-9137-4},
  url = {http://arxiv.org/abs/0712.0724},
  urldate = {2023-01-03},
  abstract = {The small object argument is a transfinite construction which, starting from a set of maps in a category, generates a weak factorisation system on that category. As useful as it is, the small object argument has some problematic aspects: it possesses no universal property; it does not converge; and it does not seem to be related to other transfinite constructions occurring in categorical algebra. In this paper, we give an “algebraic” refinement of the small object argument, cast in terms of Grandis and Tholen’s natural weak factorisation systems, which rectifies each of these three deficiencies.},
  langid = {english},
  keywords = {18A32 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  note = {Comment: 42 pages; supersedes the earlier arXiv preprint math/0702290; v2: final journal version, minor corrections only},
  file = {C:\Users\gadge\Documents\Calibre_Library\Richard Garner\Understanding the Small Object Argu (2035)\Understanding the Small Object - Richard Garner.pdf}
}

@article{gauthierTacticToeLearningProve2021,
  title = {{{TacticToe}}: {{Learning}} to {{Prove}} with {{Tactics}}},
  shorttitle = {{{TacticToe}}},
  author = {Gauthier, Thibault and Kaliszyk, Cezary and Urban, Josef and Kumar, Ramana and Norrish, Michael},
  date = {2021-02},
  journaltitle = {Journal of Automated Reasoning},
  shortjournal = {J Autom Reasoning},
  volume = {65},
  number = {2},
  eprint = {1804.00596},
  eprinttype = {arXiv},
  eprintclass = {cs},
  pages = {257--286},
  issn = {0168-7433, 1573-0670},
  doi = {10.1007/s10817-020-09580-x},
  url = {http://arxiv.org/abs/1804.00596},
  urldate = {2023-04-23},
  abstract = {We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the 7164 theorems in HOL4's standard library, whereas E prover with auto-schedule solves 34.5 percent. The success rate rises to 69.0 percent by combining the results of TacticToe and E prover.},
  keywords = {Computer Science - Artificial Intelligence,Computer Science - Logic in Computer Science},
  file = {/home/patrick/Zotero/storage/TPMM4IAA/Gauthier et al. - 2021 - TacticToe Learning to Prove with Tactics.pdf;/home/patrick/Zotero/storage/X3QA4XQ9/1804.html}
}

@online{grandisIntercategories2015,
  title = {Intercategories},
  author = {Grandis, Marco and Paré, Robert},
  date = {2015-09-11},
  eprint = {1412.0144},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1412.0144},
  urldate = {2023-09-09},
  abstract = {We introduce a 3-dimensional categorical structure which we call intercategory. This is a kind of weak triple category with three kinds of arrows, three kinds of 2-dimensional cells and one kind of 3-dimensional cells. In one dimension, the compositions are strictly associative and unitary, whereas in the other two, these laws only hold up to coherent isomorphism. The main feature is that the interchange law between the second and third compositions does not hold, but rather there is a non invertible comparison cell which satisfies some coherence conditions. We introduce appropriate morphisms of intercategory, of which there are three types, and cells relating these. We show that these fit together to produce a strict triple category of intercategories.},
  pubstate = {prepublished},
  keywords = {18D05 18D10,Mathematics - Category Theory},
  note = {Comment: 41 pages. New title and material rearranged according to the recommendations of referee. Some added examples. Final version to appear in Theory and Applications of Categories},
  file = {/home/patrick/Zotero/storage/5RNCHX2I/Grandis and Paré - 2015 - Intercategories.pdf;/home/patrick/Zotero/storage/BKS8BDAF/1412.html}
}

@article{grandisIntercategoriesFrameworkThreedimensional2017,
  title = {Intercategories: {{A}} Framework for Three-Dimensional Category Theory},
  shorttitle = {Intercategories},
  author = {Grandis, Marco and Paré, Robert},
  date = {2017-05},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {221},
  number = {5},
  pages = {999--1054},
  issn = {00224049},
  doi = {10.1016/j.jpaa.2016.08.002},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0022404916301256},
  urldate = {2023-09-07},
  langid = {english},
  file = {/home/patrick/Zotero/storage/I47UKN4T/Grandis and Paré - 2017 - Intercategories A framework for three-dimensional.pdf}
}

@article{grandisLimitsDoubleCategories1999,
  title = {Limits in Double Categories},
  author = {Grandis, Marco and Paré, Robert},
  date = {1999},
  journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
  volume = {40},
  number = {3},
  pages = {162--220},
  publisher = {Dunod éditeur, publié avec le concours du CNRS},
  url = {http://www.numdam.org/item/CTGDC_1999__40_3_162_0/},
  langid = {english},
  mrnumber = {1716779},
  zmnumber = {0939.18007},
  file = {/home/patrick/Zotero/storage/XABZG2JI/Grandis and Paré - 1999 - Limits in double categories.pdf}
}

@article{grandisNaturalWeakFactorization2006,
  title = {Natural {{Weak Factorization Systems}}},
  author = {Grandis, Marco and Tholen, Walter},
  date = {2006},
  journaltitle = {ARCHIVUM MATHEMATICUM (BRNO)},
  volume = {42},
  pages = {397--408},
  abstract = {In order to facilitate a natural choice for morphisms created by the (left or right) lifting property as used in the definition of weak factorization systems, the notion of natural weak factorization system in the category K is introduced, as a pair (comonad, monad) over K2. The link with existing notions in terms of morphism classes is given via the respective Eilenberg–Moore categories.},
  langid = {english},
  file = {/home/patrick/Zotero/storage/A6SKKJJ9/Grandis and Tholen - NATURAL WEAK FACTORIZATION SYSTEMS.pdf}
}

@article{grandisTorsionTheoriesClosure2020,
  title = {From Torsion Theories to Closure Operators and Factorization Systems},
  author = {Grandis, Marco and {Dipartimento di Matematica, Universit`a di Genova, Via Dodecaneso 35, 16146-Genova, Italy} and Janelidze, George and {Department of Mathematics and Applied Mathematics, University of Cape Town, South Africa.}},
  date = {2020-01-01},
  journaltitle = {Categories and General Algebraic Structures with Application},
  shortjournal = {CGASA},
  volume = {12},
  number = {1},
  pages = {89--121},
  issn = {23455853, 23455861},
  doi = {10.29252/CGASA.12.1.89},
  url = {http://cgasa.sbu.ac.ir/article_87116.html},
  urldate = {2023-05-29},
  langid = {english}
}

@online{grovAutomatedProofStrategy,
  title = {Towards {{Automated Proof Strategy Generalisation}}},
  author = {Grov, Gudmond and Maclean, Ewan},
  abstract = {The ability to automatically generalise (interactive) proofs and use such generalisations to dis- charge related conjectures is a very hard problem which remains unsolved; this paper shows how we hope to make a start on solving this problem. We develop a notion of goal types to capture key prop- erties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.},
  pubstate = {prepublished}
}

@online{grovAutomatedProofStrategy2013,
  title = {Towards {{Automated Proof Strategy Generalisation}}},
  author = {Grov, Gudmund and Maclean, Ewen},
  date = {2013-06-09},
  eprint = {1303.2975},
  eprinttype = {arXiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/1303.2975},
  urldate = {2023-04-24},
  abstract = {The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.},
  pubstate = {prepublished},
  keywords = {Computer Science - Artificial Intelligence,Computer Science - Logic in Computer Science},
  file = {/home/patrick/Zotero/storage/WXV3T6G9/Grov and Maclean - 2013 - Towards Automated Proof Strategy Generalisation.pdf;/home/patrick/Zotero/storage/NTTELC7U/1303.html}
}

@incollection{grovGraphicalLanguageProof2013,
  title = {A {{Graphical Language}} for {{Proof Strategies}}},
  booktitle = {Logic for {{Programming}}, {{Artificial Intelligence}}, and {{Reasoning}}},
  author = {Grov, Gudmund and Kissinger, Aleks and Lin, Yuhui},
  editor = {McMillan, Ken and Middeldorp, Aart and Voronkov, Andrei},
  editora = {Hutchison, David and Kanade, Takeo and Kittler, Josef and Kleinberg, Jon M. and Mattern, Friedemann and Mitchell, John C. and Naor, Moni and Nierstrasz, Oscar and Pandu Rangan, C. and Steffen, Bernhard and Sudan, Madhu and Terzopoulos, Demetri and Tygar, Doug and Vardi, Moshe Y. and Weikum, Gerhard},
  editoratype = {redactor},
  date = {2013},
  volume = {8312},
  pages = {324--339},
  publisher = {Springer Berlin Heidelberg},
  location = {Berlin, Heidelberg},
  doi = {10.1007/978-3-642-45221-5_23},
  url = {http://link.springer.com/10.1007/978-3-642-45221-5_23},
  urldate = {2023-04-24},
  isbn = {978-3-642-45220-8},
  file = {/home/patrick/Zotero/storage/JMAN829N/Grov et al. - 2013 - A Graphical Language for Proof Strategies.pdf}
}

@inproceedings{grovTypedMetainterpretiveLearning,
  title = {Typed Meta-Interpretive Learning for Proof Strategies},
  author = {Grov, Gudmond and Farquhar, Colin and Cropper, Andrew and Muggleton, Stephen and Bundy, Alan},
  pages = {17--32},
  location = {Kyoto, Japan},
  doi = {10.1007/978-3-319-40566-7},
  abstract = {Formal verification is increasingly used in industry. A pop- ular technique is interactive theorem proving, used for instance by Intel in HOL light. The ability to learn and re-apply proof strategies from a small set of proofs would significantly increase the productivity of these systems, and make them more cost-effective to use. Previous learning at- tempts have had limited success, which we believe is a result of missing key goal properties in the strategies. Capturing such properties will re- quire predicate invention, and the only technique we are familiar which supports this is meta-interpretive learning (MIL). We show that MIL is applicable to this problem, but that without type information it of- fers limited improvements in quality over previous work. We then extend MIL with types and give preliminary results indicating that this exten- sion learns better-quality strategies with suitable goal properties.},
  eventtitle = {25th {{Annual Conference}} on {{Inductive Logic Programming}}},
  isbn = {978-3-319-40566-7},
  langid = {english}
}

@article{hebertWeakReflectionsWeak2011,
  title = {Weak {{Reflections}} and {{Weak Factorization Systems}}},
  author = {Hébert, Michel},
  date = {2011-02},
  journaltitle = {Applied Categorical Structures},
  shortjournal = {Appl Categor Struct},
  volume = {19},
  number = {1},
  pages = {9--38},
  issn = {0927-2852, 1572-9095},
  doi = {10.1007/s10485-008-9164-1},
  url = {http://link.springer.com/10.1007/s10485-008-9164-1},
  urldate = {2023-05-29},
  langid = {english}
}

@incollection{herasML4PGComputerAlgebra2013,
  title = {{{ML4PG}} in {{Computer Algebra Verification}}},
  booktitle = {Intelligent {{Computer Mathematics}}},
  author = {Heras, Jónathan and Komendantskaya, Ekaterina},
  editor = {Carette, Jacques and Aspinall, David and Lange, Christoph and Sojka, Petr and Windsteiger, Wolfgang},
  editora = {Hutchison, David and Kanade, Takeo and Kittler, Josef and Kleinberg, Jon M. and Mattern, Friedemann and Mitchell, John C. and Naor, Moni and Nierstrasz, Oscar and Pandu Rangan, C. and Steffen, Bernhard and Sudan, Madhu and Terzopoulos, Demetri and Tygar, Doug and Vardi, Moshe Y. and Weikum, Gerhard},
  editoratype = {redactor},
  date = {2013},
  volume = {7961},
  pages = {354--358},
  publisher = {Springer Berlin Heidelberg},
  location = {Berlin, Heidelberg},
  doi = {10.1007/978-3-642-39320-4_28},
  url = {http://link.springer.com/10.1007/978-3-642-39320-4_28},
  urldate = {2023-04-24},
  isbn = {978-3-642-39320-4},
  file = {/home/patrick/Zotero/storage/F6MZXTTF/Heras and Komendantskaya - 2013 - ML4PG in Computer Algebra Verification.pdf}
}

@incollection{herasProofPatternRecognitionLemma2013,
  title = {Proof-{{Pattern Recognition}} and {{Lemma Discovery}} in {{ACL2}}},
  booktitle = {Logic for {{Programming}}, {{Artificial Intelligence}}, and {{Reasoning}}},
  author = {Heras, Jónathan and Komendantskaya, Ekaterina and Johansson, Moa and Maclean, Ewen},
  editor = {McMillan, Ken and Middeldorp, Aart and Voronkov, Andrei},
  editora = {Hutchison, David and Kanade, Takeo and Kittler, Josef and Kleinberg, Jon M. and Mattern, Friedemann and Mitchell, John C. and Naor, Moni and Nierstrasz, Oscar and Pandu Rangan, C. and Steffen, Bernhard and Sudan, Madhu and Terzopoulos, Demetri and Tygar, Doug and Vardi, Moshe Y. and Weikum, Gerhard},
  editoratype = {redactor},
  date = {2013},
  volume = {8312},
  pages = {389--406},
  publisher = {Springer Berlin Heidelberg},
  location = {Berlin, Heidelberg},
  doi = {10.1007/978-3-642-45221-5_27},
  url = {http://link.springer.com/10.1007/978-3-642-45221-5_27},
  urldate = {2023-04-24},
  isbn = {978-3-642-45221-5},
  file = {/home/patrick/Zotero/storage/T2RIIQBM/Heras et al. - 2013 - Proof-Pattern Recognition and Lemma Discovery in A.pdf}
}

@online{herasProofPatternSearch2014,
  title = {Proof {{Pattern Search}} in {{Coq}}/{{SSReflect}}},
  author = {Heras, Jónathan and Komendantskaya, Ekaterina},
  date = {2014-02-01},
  eprint = {1402.0081},
  eprinttype = {arXiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/1402.0081},
  urldate = {2023-04-24},
  abstract = {ML4PG is an extension of the Proof General interface, allowing the user to invoke machine-learning algorithms and find proof similarities in Coq/SSReect libraries. In this paper, we present three new improvements to ML4PG. First, a new method of "recurrent clustering" is introduced to collect statistical features from Coq terms. Now the user can receive suggestions about similar definitions, types and lemma statements, in addition to proof strategies. Second, Coq proofs are split into patches to capture proof strategies that could arise at different stages of a proof. Finally, we improve ML4PG's output introducing an automaton-shape representation for proof patterns.},
  pubstate = {prepublished},
  keywords = {Computer Science - Logic in Computer Science},
  file = {/home/patrick/Zotero/storage/5BKL67CC/Heras and Komendantskaya - 2014 - Proof Pattern Search in CoqSSReflect.pdf;/home/patrick/Zotero/storage/GZHGRJEL/1402.html}
}

@article{herasRecyclingProofPatterns2014,
  title = {Recycling {{Proof Patterns}} in {{Coq}}: {{Case Studies}}},
  shorttitle = {Recycling {{Proof Patterns}} in {{Coq}}},
  author = {Heras, Jónathan and Komendantskaya, Ekaterina},
  date = {2014-03},
  journaltitle = {Mathematics in Computer Science},
  shortjournal = {Math.Comput.Sci.},
  volume = {8},
  number = {1},
  pages = {99--116},
  issn = {1661-8270, 1661-8289},
  doi = {10.1007/s11786-014-0173-1},
  url = {http://link.springer.com/10.1007/s11786-014-0173-1},
  urldate = {2023-04-24},
  langid = {english},
  file = {/home/patrick/Zotero/storage/ICVC7Y8P/Heras and Komendantskaya - 2014 - Recycling Proof Patterns in Coq Case Studies.pdf}
}

@online{herasStatisticalProofPattern2013,
  title = {Statistical {{Proof Pattern Recognition}}: {{Automated}} or {{Interactive}}?},
  shorttitle = {Statistical {{Proof Pattern Recognition}}},
  author = {Heras, Jónathan and Komendantskaya, Ekaterina},
  date = {2013-03-05},
  eprint = {1303.1419},
  eprinttype = {arXiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/1303.1419},
  urldate = {2023-04-24},
  abstract = {In this paper, we compare different existing approaches employed in data mining of big proof libraries in automated and interactive theorem proving.},
  pubstate = {prepublished},
  keywords = {Computer Science - Logic in Computer Science,Computer Science - Software Engineering},
  file = {/home/patrick/Zotero/storage/TI8QFFWG/Heras and Komendantskaya - 2013 - Statistical Proof Pattern Recognition Automated o.pdf;/home/patrick/Zotero/storage/IPZKQB9D/1303.html}
}

@article{hermidaPropertiesFibFibred1999,
  title = {Some Properties of {{Fib}} as a Fibred 2-Category},
  author = {Hermida, Claudio},
  date = {1999-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {134},
  number = {1},
  pages = {83--109},
  issn = {00224049},
  doi = {10.1016/S0022-4049(97)00129-1},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0022404997001291},
  urldate = {2023-10-05},
  langid = {english}
}

@book{hirschhornModelCategoriesTheir2003,
  title = {Model Categories and Their Localizations},
  author = {Hirschhorn, Philip S.},
  date = {2003},
  series = {Mathematical Surveys and Monographs},
  number = {v. 99},
  publisher = {American Mathematical Society},
  location = {Providence, RI},
  isbn = {978-0-8218-3279-0},
  pagetotal = {457},
  keywords = {Homotopy theory,Model categories (Mathematics)}
}

@book{hoveyModelCategories1999,
  title = {Model Categories},
  author = {Hovey, Mark},
  date = {1999},
  series = {Mathematical Surveys and Monographs},
  number = {v. 63},
  publisher = {American Mathematical Society},
  location = {Providence, R.I},
  isbn = {978-0-8218-1359-1},
  pagetotal = {209},
  keywords = {Complexes,Homotopy theory,Model categories (Mathematics)}
}

@book{inoueInductiveLogicProgramming2016,
  title = {Inductive {{Logic Programming}}: 25th {{International Conference}}, {{ILP}} 2015, {{Kyoto}}, {{Japan}}, {{August}} 20-22, 2015, {{Revised Selected Papers}}},
  shorttitle = {Inductive {{Logic Programming}}},
  editor = {Inoue, Katsumi and Ohwada, Hayato and Yamamoto, Akihiro},
  date = {2016},
  series = {Lecture {{Notes}} in {{Artificial Intelligence}}},
  edition = {1st ed. 2016},
  number = {9575},
  publisher = {Springer International Publishing : Imprint: Springer},
  location = {Cham},
  doi = {10.1007/978-3-319-40566-7},
  abstract = {This book constitutes the thoroughly refereed post-conference proceedings of the 25th International Conference on Inductive Logic Programming, ILP 2015, held in Kyoto, Japan, in August 2015. The 14 revised papers presented were carefully reviewed and selected from 44 submissions. The papers focus on topics such as theories, algorithms, representations and languages, systems and applications of ILP, and cover all areas of learning in logic, relational learning, relational data mining, statistical relational learning, multi-relational data mining, relational reinforcement learning, graph mining, connections with other learning paradigms, among others},
  isbn = {978-3-319-40566-7},
  pagetotal = {1},
  keywords = {Artificial intelligence,Artificial Intelligence,Computer logic,Computer programming,Data mining,Data Mining and Knowledge Discovery,Logics and Meanings of Programs,Mathematical logic,Mathematical Logic and Formal Languages,Programming Techniques},
  file = {/home/patrick/Zotero/storage/DGCQQJ63/Inoue et al. - 2016 - Inductive Logic Programming 25th International Co.pdf}
}

@book{jacobsCategoricalLogicType,
  title = {Categorical {{Logic}} and {{Type Theory}}},
  author = {Jacobs, Bart},
  series = {Studies in {{Logic}} and the {{Foundations}} of {{Mathematics}}},
  volume = {141},
  publisher = {Elsevier},
  isbn = {0 444 50170 3}
}

@article{jacobsSemanticsWeakeningContraction1994,
  title = {Semantics of Weakening and Contraction},
  author = {Jacobs, Bart},
  date = {1994-09},
  journaltitle = {Annals of Pure and Applied Logic},
  shortjournal = {Annals of Pure and Applied Logic},
  volume = {69},
  number = {1},
  pages = {73--106},
  issn = {01680072},
  doi = {10.1016/0168-0072(94)90020-5},
  url = {https://linkinghub.elsevier.com/retrieve/pii/0168007294900205},
  urldate = {2023-02-18},
  langid = {english},
  file = {/home/patrick/Zotero/storage/XMETGDNB/Jacobs - 1994 - Semantics of weakening and contraction.pdf}
}

@book{jamesHandbookAlgebraicTopology1995,
  title = {Handbook of Algebraic Topology},
  editor = {James, I. M.},
  date = {1995},
  publisher = {Elsevier Science B.V},
  location = {Amsterdam ; New York},
  isbn = {978-0-444-81779-2},
  pagetotal = {1324},
  keywords = {Algebraic topology}
}

@article{jamnikAutomaticLearningProof2003,
  title = {Automatic {{Learning}} of {{Proof Methods}} in {{Proof Planning}}},
  author = {Jamnik, M.},
  date = {2003-11-01},
  journaltitle = {Logic Journal of IGPL},
  shortjournal = {Logic Journal of IGPL},
  volume = {11},
  number = {6},
  pages = {647--673},
  issn = {1367-0751, 1368-9894},
  doi = {10.1093/jigpal/11.6.647},
  url = {https://academic.oup.com/jigpal/article-lookup/doi/10.1093/jigpal/11.6.647},
  urldate = {2023-04-24},
  langid = {english}
}

@book{johnson2dimensionalCategories2021,
  title = {2-Dimensional Categories},
  author = {Johnson, Niles and Yau, Donald Y.},
  date = {2021},
  edition = {First edition},
  publisher = {Oxford University Press},
  location = {Oxford, United Kingdom ; New York, NY},
  abstract = {2--Dimensional Categories provides an introduction to 2-categories and bicategories, assuming only the most elementary aspects of category theory. A review of basic category theory is followed by a systematic discussion of 2-/bicategories; pasting diagrams; lax functors; 2-/bilimits; the Duskin nerve; the 2-nerve; internal adjunctions; monads in bicategories; 2-monads; biequivalences; the Bicategorical Yoneda Lemma; and the Coherence Theorem for bicategories. Grothendieck fibrations and the Grothendieck construction are discussed next, followed by tricategories, monoidal bicategories, the Gray tensor product, and double categories. Completely detailed proofs of several fundamental but hard-to-find results are presented for the first time. With exercises and plenty of motivation and explanation, this book is useful for both beginners and experts.--},
  isbn = {978-0-19-887137-8},
  pagetotal = {615},
  keywords = {Categories (Mathematics)},
  annotation = {OCLC: on1198975671}
}

@inproceedings{kammarAlgebraicFoundationsEffectdependent2012,
  title = {Algebraic Foundations for Effect-Dependent Optimisations},
  booktitle = {Proceedings of the 39th Annual {{ACM SIGPLAN-SIGACT}} Symposium on {{Principles}} of Programming Languages},
  author = {Kammar, Ohad and Plotkin, Gordon D.},
  date = {2012-01-25},
  pages = {349--360},
  publisher = {ACM},
  location = {Philadelphia PA USA},
  doi = {10.1145/2103656.2103698},
  url = {https://dl.acm.org/doi/10.1145/2103656.2103698},
  urldate = {2023-02-18},
  eventtitle = {{{POPL}} '12: {{The}} 39th {{Annual ACM SIGPLAN-SIGACT Symposium}} on {{Principles}} of {{Programming Languages}}},
  isbn = {978-1-4503-1083-3},
  langid = {english}
}

@thesis{kammarAlgebraicTheoryTypeandEffect2014,
  title = {An {{Algebraic Theory}} of {{Type-and-Effect Systems}}},
  author = {Kammar, Ohad},
  date = {2014},
  institution = {University of Oxford},
  url = {http://www.cs.ox.ac.uk/people/ohad.kammar/thesis/},
  abstract = {We present a general semantic account of Gifford-style type-and-effect systems. These type systems provide lightweight static analyses annotating program phrases with the sets of possible computational effects they may cause, such as memory access and modification, exception raising, and non-deterministic choice. The analyses are used, for example, to justify the program transformations typically used in optimising com- pilers, such as code reordering and inlining. Despite their existence for over two decades, there is no prior comprehensive theory of type-and-effect systems accounting for their syntax and semantics, and justifying their use in effect-dependent program transformation. We achieve this generality by recourse to the theory of algebraic effects, a de- velopment of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with the effect operations. Our first main contribution is the uniform construction of semantic models for type- and-effect analysis by a process we call conservative restriction. Our construction re- quires an algebraic model of the unannotated programming language and a relevant notion of predicate. It then generates a model for Gifford-style type-and-effect anal- ysis. This uniform construction subsumes existing ad-hoc models for type-and-effect systems, and is applicable in all cases in which the semantics can be given via enriched Lawvere theories. Our second main contribution is a demonstration that our theory accounts for the various aspects of Gifford-style effect systems. We begin with a version of Levy’s Call- by-push-value that includes algebraic effects. We add effect annotations, and design a general type-and-effect system for such call-by-push-value variants. The annotated language can be thought of as an intermediate representation used for program optimi- sation. We relate the unannotated semantics to the conservative restriction semantics, and establish the soundness of program transformations based on this effect analysis. We develop and classify a range of validated transformations, generalising many ex- isting ones and adding some new ones. We also give modularly-checkable sufficient conditions for the validity of these optimisations. In the final part of this thesis, we demonstrate our theory by analysing a simple example language involving global state with multiple regions, exceptions, and non- determinism. We give decision procedures for the applicability of the various effect- dependent transformations, and establish their soundness and completeness.},
  langid = {english},
  pagetotal = {342}
}

@book{kirchnerAutomatedDeductionCADE151998,
  title = {Automated Deduction, {{CADE-15}}: 15th {{International Conference}} on {{Automated Deduction}}, {{Lindau}}, {{Germany}}, {{July}} 5-10, 1998: Proceedings},
  shorttitle = {Automated Deduction, {{CADE-15}}},
  editor = {Kirchner, Claude and Kirchner, H.},
  date = {1998},
  series = {Lecture Notes in Computer Science},
  number = {1421. Lecture notes in artificial intelligence},
  publisher = {Springer},
  location = {Berlin ; New York},
  eventtitle = {International {{Conference}} on {{Automated Deduction}}},
  isbn = {978-3-540-64675-4},
  pagetotal = {441},
  keywords = {Automatic theorem proving,Congresses,Logic Symbolic and mathematical}
}

@article{kleisliConstructionStandardComplexes1974,
  title = {On the Construction of Standard Complexes},
  author = {Kleisli, Heinrich},
  date = {1974-06},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {4},
  number = {3},
  pages = {243--260},
  issn = {00224049},
  doi = {10.1016/0022-4049(74)90005-X},
  url = {https://linkinghub.elsevier.com/retrieve/pii/002240497490005X},
  urldate = {2023-06-25},
  langid = {english}
}

@article{kleisliConstructionStandardComplexes1974a,
  title = {On the Construction of Standard Complexes},
  author = {Kleisli, Heinrich},
  date = {1974},
  journaltitle = {Journal of Pure and Applied Algebra},
  volume = {4},
  pages = {243--260},
  abstract = {By a standard complex we understand a complex of the following type: the complex first used by Eilenberg and ,MacLa.ne to define the cohomology of groups; the complex first used by Hochschild to defme the cohomology of an associative al- gebra (cf. [6] or [IO) ); the complexes introduced by And\& Barr and Beck in [ 1, 4.5). N those complexes are constructed according to a common pattern. We start with the foBowing data: A cotriple (comonad) C in a category A (which can be chosen to be small) and a set- or group-valued functor F on A. There is simplicial objet t X\_ = (X, , d’), a o ( where we drop the degeneracy operators) in the functor category AA, which is obtained from c by a standard construction due to Godement (cf. [ 8, appendice) ). Composing X. with the functor F we obtain a simplicial object FX\_ = (FX,, Fdi),ro in the functor category Ed or A@. in the latter case one usually considers the associated chain complex (and if the degeneracy operators are brought dong, sometimes its normalization), The resulting functorial complex is what we call a star\&ant txmpl\textasciitilde x. The aim of this paper is to construct standard complexes which are (homotopy) equivaien t to classical geometric complexes by using some simple arguments of ca- tegorical algebra. Moreover, we want to s!tow that the introduction of such standard complexes is useful by giving a few immediate applications leading in a natural way to classical results such as t.hlr: topologic4 iinvariance or’ simplicial homology for poly- hedra and de Rham’s theorem. I am indepted to Michael Barr and to Claude Auderset for many conversations which gave the paper its present form. The former pointed out to me the preprint of a paper by Rinehart [ B 21 in which singular and simplicial homology are treated as satellites relative to a pro,jective class, a paper which shaped the choice of the ap- plications presented here. He also knew of the cotriple E of Section 5 (without the help of Theorem 3.3). The latter observed that the double complexes in Sections 7 and \$ hapi-en to be isomorphic to the double complexes used by Weil in a classical proof of Leray’s theorem and of de Rham’s theorem (cf. f IS] ). It should be men- tioned, however, that our proofs are different from those of Weil insofar as we do not need to know the explicit form of those double complexes.}
}

@article{kleisliEveryStandardConstruction1965,
  title = {Every Standard Construction Is Induced by a Pair of Adjoint Functors},
  author = {Kleisli, H.},
  date = {1965},
  journaltitle = {Proceedings of the American Mathematical Society},
  shortjournal = {Proc. Amer. Math. Soc.},
  volume = {16},
  number = {3},
  pages = {544--546},
  issn = {0002-9939, 1088-6826},
  doi = {10.1090/S0002-9939-1965-0177024-4},
  url = {https://www.ams.org/proc/1965-016-03/S0002-9939-1965-0177024-4/},
  urldate = {2023-02-25},
  langid = {english},
  file = {/home/patrick/Zotero/storage/YKR7L2BK/Kleisli - 1965 - Every standard construction is induced by a pair o.pdf}
}

@article{kleisliResolutionsDansCategories1967,
  title = {Résolutions Dans Les Catégories Avec Multiplication},
  author = {Kleisli, H.},
  date = {1967},
  journaltitle = {C. R. Acad. Sci. Paris},
  volume = {264},
  pages = {11--16}
}

@article{kockBilinearityCartesianclosedMonads1971,
  title = {Bilinearity and Cartesian-Closed Monads},
  author = {Kock, Anders},
  date = {1971},
  journaltitle = {Mathematica Scandinavica},
  volume = {29},
  number = {2},
  eprint = {24491025},
  eprinttype = {jstor},
  pages = {161--74},
  url = {http://www.jstor.org/stable/24491025},
  abstract = {The observation that universal algebra can be treated "in a coordinate free way", using monads, together with the observation that many tech niques available in the category of sets are available in any symmetric monoidal closed category V, makes it possible, by combined use of the monad language and the closed category language, to describe some of the elementary notions of universal algebra in an element-free way. Syntactically, such a description no longer has variables ranging over the set of elements in an algebra, but rather over the class of algebras itself. In particular, though the monad-theoretic treatment allows for infinitary algebras, the notions formulated here are all formulated in a finitary way. For example, one can formulate the notion of "algebra, where every operation is a homomorphism with respect to any operation". This was done in [3], [4], and [5], The notion to be described here is that of a "function in two vari ables which is a homomorphism in each variable separately." This concept of "bilinearity" is used in the main Section 2, which deals with cartesian closed categories. The main theorem is Theorem 2.6 which says that a monad on a cartesian closed category, whose functor part commutes with products satisfies: (i) it carries a unique structure as strong monad; and (ii) this structure makes the monad commutative in the sense of [3]; and (iii) the category of algebras for it is cartesian closed. Monads of this kind we call cartesian closed (Definition 2.7). They can also be characterized as commutative monads for which a map "is bi linear if and only if it is linear" (Theorem 2.5). The two implications in this "if and only if" are investigated separately in Theorem 2.1 and Proposition 2.3, the first describing the notion of "affine monad".}
}

@article{kockClosedCategoriesGenerated1971,
  title = {Closed Categories Generated by Commutative Monads},
  author = {Kock, Anders},
  date = {1971-11},
  journaltitle = {Journal of the Australian Mathematical Society},
  shortjournal = {J. Aust. Math. Soc.},
  volume = {12},
  number = {4},
  pages = {405--424},
  issn = {0004-9735},
  doi = {10.1017/S1446788700010272},
  url = {https://www.cambridge.org/core/product/identifier/S1446788700010272/type/journal_article},
  urldate = {2023-02-04},
  abstract = {The notion of commutative monad was defined by the author in [4]. The content of the present paper may briefly be stated: The category of algebras for a commutative monad can in a canonical way be made into a closed category, the two adjoint functors connecting the category of algebras with the base category are in a canonical way closed functors, and the front- and end-adjunctions are closed transformations. (The terms ‘Closed Category’ etc. are from the paper [2] by Eilenberg and Kelly). In particular, the monad itself is a ‘closed monad’; this fact was also proved in [4].},
  langid = {english}
}

@article{kockMonadsSymmetricMonoidal1970,
  title = {Monads on Symmetric Monoidal Closed Categories},
  author = {Kock, Anders},
  date = {1970-12},
  journaltitle = {Archiv der Mathematik},
  shortjournal = {Arch. Math},
  volume = {21},
  number = {1},
  pages = {1--10},
  issn = {0003-889X, 1420-8938},
  doi = {10.1007/BF01220868},
  url = {http://link.springer.com/10.1007/BF01220868},
  urldate = {2023-02-04},
  langid = {english}
}

@article{kockStrongFunctorsMonoidal1972,
  title = {Strong Functors and Monoidal Monads},
  author = {Kock, Anders},
  date = {1972-12},
  journaltitle = {Archiv der Mathematik},
  shortjournal = {Arch. Math},
  volume = {23},
  number = {1},
  pages = {113--120},
  issn = {0003-889X, 1420-8938},
  doi = {10.1007/BF01304852},
  url = {http://link.springer.com/10.1007/BF01304852},
  urldate = {2023-02-04},
  langid = {english}
}

@article{komendantskayaMachineLearningProof2012,
  title = {Machine {{Learning}} in {{Proof General}}: {{Interfacing Interfaces}}},
  shorttitle = {Machine {{Learning}} in {{Proof General}}},
  author = {Komendantskaya, Ekaterina and Heras, Jónathan and Grov, Gudmund},
  date = {2012},
  publisher = {arXiv},
  doi = {10.48550/ARXIV.1212.3618},
  url = {https://arxiv.org/abs/1212.3618},
  urldate = {2023-04-24},
  abstract = {We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.},
  version = {2},
  keywords = {Artificial Intelligence (cs.AI),FOS: Computer and information sciences,I.2.6; F.4.1,Logic in Computer Science (cs.LO),Machine Learning (cs.LG)},
  note = {\subsection{Other}

In Proceedings UITP 2012, arXiv:1307.1528}
}

@online{konigVanKampenColimits2018,
  title = {Van {{Kampen Colimits}} and {{Path Uniqueness}}},
  author = {König, Harald and Wolter, Uwe},
  date = {2018-04-24},
  eprint = {1710.09784},
  eprinttype = {arXiv},
  eprintclass = {math},
  doi = {10.23638/LMCS-14(2:5)2018},
  url = {http://arxiv.org/abs/1710.09784},
  urldate = {2023-06-25},
  abstract = {Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, i.e, categories of objects that can be represented as algebras as well as coalgebras, e.g., the category of directed graphs. Multimodeling requires to construct colimits of models, decomposition is given by pullback. Compositionality requires an exact interplay of these operations, i.e., diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible. In this paper we state a necessary and sufficient yet efficiently checkable condition for the Van Kampen property to hold in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Soboci\textbackslash '\{n\}ski the fact that the Van Kampen property reveals a presheaf-based structural uniqueness feature.},
  pubstate = {prepublished},
  keywords = {18A15 18A25,Mathematics - Category Theory},
  file = {/home/patrick/Zotero/storage/5W2QYERJ/König and Wolter - 2018 - Van Kampen Colimits and Path Uniqueness.pdf;/home/patrick/Zotero/storage/UDCMR2IC/1710.html}
}

@article{lambertCartesianDoubleTheories2024,
  title = {Cartesian Double Theories: {{A}} Double-Categorical Framework for Categorical Doctrines},
  shorttitle = {Cartesian Double Theories},
  author = {Lambert, Michael and Patterson, Evan},
  date = {2024-05},
  journaltitle = {Advances in Mathematics},
  shortjournal = {Advances in Mathematics},
  volume = {444},
  pages = {109630},
  issn = {00018708},
  doi = {10.1016/j.aim.2024.109630},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S0001870824001452},
  urldate = {2025-09-05},
  langid = {english},
  file = {/home/patrick/Zotero/storage/TEYG96Q4/Lambert and Patterson - 2024 - Cartesian double theories A double-categorical framework for categorical doctrines.pdf}
}

@article{leinsterBasicBicategories1998,
  title = {Basic {{Bicategories}}},
  author = {Leinster, Tom},
  date = {1998},
  publisher = {arXiv},
  doi = {10.48550/ARXIV.MATH/9810017},
  url = {https://arxiv.org/abs/math/9810017},
  urldate = {2023-10-04},
  abstract = {A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem.},
  version = {1},
  keywords = {Category Theory (math.CT),FOS: Mathematics},
  note = {\subsection{Other}

11 pages; LaTeX 2e with Paul Taylor's diagram macros}
}

@book{leinsterHigherOperadsHigher2004,
  title = {Higher Operads, Higher Categories},
  author = {Leinster, Tom},
  date = {2004},
  series = {London {{Mathematical Society}} Lecture Note Series},
  number = {298},
  publisher = {Cambridge University Press},
  location = {Cambridge, UK ; New York},
  isbn = {978-0-521-53215-0},
  pagetotal = {433},
  keywords = {Categories (Mathematics),Operads}
}

@online{liLEMMABootstrappingHighLevel2022,
  title = {{{LEMMA}}: {{Bootstrapping High-Level Mathematical Reasoning}} with {{Learned Symbolic Abstractions}}},
  shorttitle = {{{LEMMA}}},
  author = {Li, Zhening and Poesia, Gabriel and Costilla-Reyes, Omar and Goodman, Noah and Solar-Lezama, Armando},
  date = {2022-11-15},
  eprint = {2211.08671},
  eprinttype = {arXiv},
  eprintclass = {cs},
  url = {http://arxiv.org/abs/2211.08671},
  urldate = {2023-04-24},
  abstract = {Humans tame the complexity of mathematical reasoning by developing hierarchies of abstractions. With proper abstractions, solutions to hard problems can be expressed concisely, thus making them more likely to be found. In this paper, we propose Learning Mathematical Abstractions (LEMMA): an algorithm that implements this idea for reinforcement learning agents in mathematical domains. LEMMA augments Expert Iteration with an abstraction step, where solutions found so far are revisited and rewritten in terms of new higher-level actions, which then become available to solve new problems. We evaluate LEMMA on two mathematical reasoning tasks--equation solving and fraction simplification--in a step-by-step fashion. In these two domains, LEMMA improves the ability of an existing agent, both solving more problems and generalizing more effectively to harder problems than those seen during training.},
  pubstate = {prepublished},
  keywords = {Computer Science - Artificial Intelligence},
  note = {Comment: 10 pages, 2 figures; to appear in 2nd MATH-AI Workshop at NeurIPS'22},
  file = {/home/patrick/Zotero/storage/CFUUWPSG/Li et al. - 2022 - LEMMA Bootstrapping High-Level Mathematical Reaso.pdf;/home/patrick/Zotero/storage/ZD6RJG46/2211.html}
}

@misc{Ltac2Documentation,
  title = {Ltac2 Documentation},
  url = {https://coq.inria.fr/refman/proof-engine/ltac2.html}
}

@book{maclaneCategoriesWorkingMathematician1998,
  title = {Categories for the Working Mathematician},
  author = {Mac Lane, Saunders},
  date = {1998},
  series = {Graduate Texts in Mathematics},
  edition = {2nd ed},
  number = {5},
  publisher = {Springer},
  location = {New York},
  isbn = {978-0-387-98403-2},
  pagetotal = {314},
  keywords = {Categories (Mathematics)},
  file = {/home/patrick/Zotero/storage/99QAEQAQ/Categories for the Working Mathematician, - Saunders Mac Lane.pdf}
}

@book{maclaneSheavesGeometryLogic1992,
  title = {Sheaves in Geometry and Logic: A First Introduction to Topos Theory},
  shorttitle = {Sheaves in Geometry and Logic},
  author = {Mac Lane, Saunders and Moerdijk, Ieke},
  date = {1992},
  series = {Universitext},
  publisher = {Springer-Verlag},
  location = {New York},
  isbn = {978-0-387-97710-2},
  langid = {english},
  pagetotal = {627},
  keywords = {Toposes}
}

@inreference{maresRelevanceLogic2022,
  title = {Relevance Logic},
  booktitle = {The {{Stanford Encyclopedia}} of {{Philosophy}}},
  author = {Mares, Edwin},
  date = {2022},
  edition = {Fall 2022},
  publisher = {Metaphysics Research Lab, Stanford University},
  url = {https://plato.stanford.edu/archives/fall2022/entries/logic-relevance/},
  abstract = {Relevance logics are non-classical logics. Called ‘relevant logics’ in Britain and Australasia, these systems developed as attempts to avoid the paradoxes of material and strict implication. These so-called paradoxes are valid conclusions that follow from the definitions of material and strict implication but are seen, by some, as problematic. For example, the material implication (p→q) is true whenever p is false or q is true — i.e., (¬p∨q). So if p is true, then the material implication is true when q is true. Among the paradoxes of material implication are the following: p→(q→p),¬p→(p→q),(p→q)∨(q→r). The first asserts that every proposition implies a true one; the second that a false proposition implies every proposition, and the third that for any three propositions, either the first implies the second or the second implies the third. Similarly, the strict implication (p→q) is true whenever it is not possible that p is true and q is false — i.e., ¬⋄(p\&¬q) . Among the paradoxes of strict implication are the following: (p\&¬p)→q,p→(q→q),p→(q∨¬q). The first asserts that a contradiction strictly implies every proposition; the second and third imply that every proposition strictly implies a tautology. Many philosophers, beginning with Hugh MacColl (1908), have claimed that these theses are counterintuitive. They claim that these formulae fail to be valid if we interpret → as representing the concept of implication that we have before we learn classical logic. Relevance logicians claim that what is unsettling about these so-called paradoxes is that in each of them the antecedent seems irrelevant to the consequent. In addition, relevance logicians have had qualms about certain inferences that classical logic makes valid. For example, consider the classically valid inference     The moon is made of green cheese. Therefore, either it is raining in Ecuador now or it is not.  Again here there seems to be a failure of relevance. The conclusion seems to have nothing to do with the premise. Relevance logicians have attempted to construct logics that reject theses and arguments that commit “fallacies of relevance”.}
}

@article{mayClassifyingSpacesFibrations1975,
  title = {Classifying Spaces and Fibrations},
  author = {May, J. Peter},
  date = {1975},
  journaltitle = {Memoirs of the American Mathematical Society},
  shortjournal = {Memoirs of the AMS},
  volume = {1},
  number = {155},
  issn = {0065-9266, 1947-6221},
  doi = {10.1090/memo/0155},
  url = {http://www.ams.org/memo/0155},
  urldate = {2023-02-19},
  langid = {english}
}

@book{maySimplicialObjectsAlgebraic1967,
  title = {Simplicial Objects in Algebraic Topology},
  author = {May, Jon Peter},
  date = {1967},
  series = {Midway Reprint},
  publisher = {Univ. of Chicago Press},
  location = {Chicago},
  isbn = {978-0-226-51180-1},
  pagetotal = {161},
  note = {Bibliography: p157-161}
}

@article{meyerBarCobarConstructions1984,
  title = {Bar and Cobar Constructions, {{I}}},
  author = {Meyer, Jean-Pierre},
  date = {1984-08-01},
  journaltitle = {Journal of Pure and Applied Algebra},
  shortjournal = {Journal of Pure and Applied Algebra},
  volume = {33},
  number = {2},
  pages = {163--207},
  issn = {0022-4049},
  doi = {10.1016/0022-4049(84)90005-7},
  url = {https://www.sciencedirect.com/science/article/pii/0022404984900057},
  urldate = {2022-12-23},
  langid = {english},
  file = {/home/patrick/Zotero/storage/WQ8KVGZW/Meyer - 1984 - Bar and cobar constructions, I.pdf;/home/patrick/Zotero/storage/EB2KG4F4/0022404984900057.html}
}

@report{millerOverviewLambdaProlog1988,
  type = {Technical Report},
  title = {An {{Overview}} of {{Lambda-Prolog}}},
  author = {Miller, Dale and Nadathur, Gopalan},
  date = {1988-06},
  number = {MS-CIS-88-40},
  institution = {{University of Pennsylvania Department of Computer and Information Science}},
  location = {Philadelphia PA USA},
  url = {https://repository.upenn.edu/cis_reports/595/},
  abstract = {λ-Prolog is a logic programming language that extends Prolog by incorporating notions of higher-order functions, λ-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various aspects of an experimental implementation of λ-Prolog.}
}

@inproceedings{moggiComputationalLambdacalculusMonads1989,
  title = {Computational Lambda-Calculus and Monads},
  booktitle = {[1989] {{Proceedings}}. {{Fourth Annual Symposium}} on {{Logic}} in {{Computer Science}}},
  author = {Moggi, E.},
  date = {1989},
  pages = {14--23},
  publisher = {IEEE Comput. Soc. Press},
  location = {Pacific Grove, CA, USA},
  doi = {10.1109/LICS.1989.39155},
  url = {http://ieeexplore.ieee.org/document/39155/},
  urldate = {2023-02-04},
  abstract = {The λ-calculus is considered an useful mathematical tool in the study of programming languages. However, if one uses βη-conversion to prove equivalence of programs, then a gross simplification1 is introduced. We give a calculus based on a categorical semantics for computations, which provides a correct basis for proving equivalence of programs, independent from any specific computational model.},
  eventtitle = {[1989] {{Proceedings}}. {{Fourth Annual Symposium}} on {{Logic}} in {{Computer Science}}},
  isbn = {978-0-8186-1954-0},
  langid = {english},
  file = {/home/patrick/Zotero/storage/5M4CB9Q9/Moggi - 1989 - Computational lambda-calculus and monads.pdf}
}

@article{moggiNotionsComputationMonads1991,
  title = {Notions of Computation and Monads},
  author = {Moggi, Eugenio},
  date = {1991-07},
  journaltitle = {Information and Computation},
  shortjournal = {Information and Computation},
  volume = {93},
  number = {1},
  pages = {55--92},
  issn = {08905401},
  doi = {10.1016/0890-5401(91)90052-4},
  url = {https://linkinghub.elsevier.com/retrieve/pii/0890540191900524},
  urldate = {2023-02-04},
  abstract = {The λ-calculus is considered an useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values), that may jeopardise the applicability of theoretical results. In this paper we introduce calculi based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs, for a wide range of notions of computation.},
  langid = {english},
  file = {/home/patrick/Zotero/storage/JYSNLAF4/Moggi - 1991 - Notions of computation and monads.pdf}
}

@incollection{mooreCartansConstructionsHomology1976,
  title = {Cartan's Constructions, the Homology of {{K}}(\$\textbackslash pi\$, n)'s, and Some Later Developments},
  booktitle = {Colloque Analyse et Topologie},
  author = {Moore, John C. and {Collectif}},
  date = {1976},
  series = {Astérisque},
  number = {32--33},
  publisher = {Société mathématique de France},
  url = {http://www.numdam.org/item/AST_1976__32-33__173_0/},
  langid = {english},
  mrnumber = {413090},
  zmnumber = {0339.55001}
}

@online{ozornovaUnitTotalDecalage2020,
  title = {The Unit of the Total D\textbackslash 'ecalage Adjunction},
  author = {Ozornova, Viktoriya and Rovelli, Martina},
  date = {2020-05-22},
  eprint = {1711.03451},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1711.03451},
  urldate = {2023-01-04},
  abstract = {We consider the d´ecalage construction Dec and its right adjoint T . These functors are induced on the category of simplicial objects valued in any bicomplete category C by the ordinal sum. We identify T Dec X with the path object X∆[1] for any simplicial object X. We then use this formula to produce an explicit retracting homotopy for the unit X → T Dec X of the adjunction (Dec, T ). When C is a category of objects of an algebraic nature, we then show that the unit is a weak equivalence of simplicial objects in C.},
  langid = {english},
  pubstate = {prepublished},
  keywords = {55U10 18G30 55P10,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  note = {Comment: Final version},
  file = {C:\Users\gadge\Documents\Calibre_Library\Viktoriya Ozornova\The Unit of the Total Decalage Adjunction (1962)\The Unit of the Total Decalage Adjunction - Viktoriya Ozornova.pdf}
}

@article{pareCompositionModulesLax2013,
  title = {Composition of {{Modules}} for {{Lax Functors}}},
  author = {Paré, Robert},
  date = {2013-04-03},
  journaltitle = {Theory and Applications of Categories},
  shortjournal = {Theory appl. categ.},
  volume = {27},
  number = {16},
  pages = {393--444},
  issn = {1201-561X},
  url = {http://www.tac.mta.ca/tac/volumes/27/16/27-16abs.html},
  abstract = {We study the composition of modules between lax functors of weak double categories. We adapt the bicategorical notion of local cocompleteness to weak double categories, which the codomain of our lax functors will be assumed to satisfy. We introduce a notion of factorization of cells, which most weak double categories of interest possess, and which is sufficient to guarantee the strong representability of composites of modules between lax functors whose domain satisfies it.},
  langid = {english}
}

@online{parePersistentDoubleLimits,
  title = {Persistent Double Limits and Flexible Weighted Limits},
  author = {Paré, Robert and Grandis, Marco},
  url = {https://www.mscs.dal.ca/~pare/DblPrs2.pdf},
  abstract = {This is the sequel of an article on persistent double limits in weak double categories. Here we consider their links with flexible weighted limits in 2-categories.},
  pubstate = {prepublished}
}

@article{parePersistentDoubleLimits2019,
  title = {Persistent {{Double Limits}}},
  author = {Paré, Robert and Grandis, Marco},
  date = {2019},
  journaltitle = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
  shortjournal = {Cahiers},
  volume = {LX},
  number = {3},
  pages = {255--297},
  issn = {2681-2363},
  url = {https://cahierstgdc.com/wp-content/uploads/2019/07/GRANDIS_PARE_LX-3.pdf},
  urldate = {2025-11-03},
  langid = {english}
}

@article{pareYonedaTheoryDouble2011,
  title = {Yoneda Theory for Double Categories},
  author = {Paré, Robert},
  date = {2011},
  journaltitle = {Theory and Applications of Categories},
  shortjournal = {Theory appl. categ.},
  volume = {25},
  number = {17},
  pages = {436--489},
  issn = {1201-561X},
  url = {http://www.tac.mta.ca/tac/volumes/25/17/25-17.pdf},
  abstract = {Representables for double categories are defined to be lax morphisms into a certain double category of sets. We show that horizontal transformations from rep- resentables into lax morphisms correspond to elements of that lax morphism. Vertical arrows give rise to modules between representables. We establish that the Yoneda em- bedding is a strong morphism of lax double categories which is horizontally full and faithful and dense.},
  langid = {english}
}

@online{parlantPreservationEquationsMonoidal2020,
  title = {Preservation of {{Equations}} by {{Monoidal Monads}}},
  author = {Parlant, Louis and Rot, Jurriaan and Silva, Alexandra and Westerbaan, Bas},
  date = {2020-07-07},
  eprint = {2001.06348},
  eprinttype = {arXiv},
  eprintclass = {cs, math},
  url = {http://arxiv.org/abs/2001.06348},
  urldate = {2023-02-18},
  abstract = {If a monad \$T\$ is monoidal, then operations on a set \$X\$ can be lifted canonically to operations on \$TX\$. In this paper we study structural properties under which \$T\$ preserves equations between those operations. It has already been shown that any monoidal monad preserves linear equations; affine monads preserve drop equations (where some variable appears only on one side, such as \$x\textbackslash cdot y = y\$) and relevant monads preserve dup equations (where some variable is duplicated, such as \$x \textbackslash cdot x = x\$). We start the paper by showing a converse: if the monad at hand preserves a drop equation, then it must be affine. From this, we show that the problem whether a given (drop) equation is preserved is undecidable. A converse for relevance turns out to be more subtle: preservation of certain dup equations implies a weaker notion which we call \$n\$-relevance. Finally, we identify the subclass of equations such that their preservation is equivalent to relevance.},
  pubstate = {prepublished},
  keywords = {Computer Science - Logic in Computer Science,Mathematics - Category Theory},
  file = {/home/patrick/Zotero/storage/5WEGVI9W/Parlant et al. - 2020 - Preservation of Equations by Monoidal Monads.pdf;/home/patrick/Zotero/storage/RBWNK7BS/2001.html}
}

@inproceedings{pedrotLtac2TacticalWarfare2019,
  title = {Ltac2 - {{Tactical Warfare}}},
  author = {Pedrot, Pierre-Marie},
  date = {2019-01-19},
  location = {Lisbon, Portugal},
  url = {https://www.xn--pdrot-bsa.fr/articles/coqpl2019.pdf},
  abstract = {We present Ltac2, a proposal for the replacement of the Ltac tactic language that is shipped with Coq as the default inter- face to build up proofs interactively. Ltac2 is primarily mo- tivated by two antagonistic desires, namely extending the expressivity and regularity of the historical tactic language of Coq while maintaining a strong backward compatibility. We thereafter give a bird’s eye view of the features and se- mantics of the current state of Ltac2.},
  eventtitle = {The {{Fifth International Workshop}} on {{Coq}} for {{Programming Languages CoqPL}} 2019}
}

@inproceedings{pengzhouREFACTORLearningExtract2021,
  title = {{{REFACTOR}}: {{Learning}} to Extract Theorems from Proofs},
  author = {Peng Zhou, Jin and Wu, Yuhuai and Li, Qiyang and Grosse, Roger},
  date = {2021},
  abstract = {Human mathematicians are often good at recognizing modular and reusable the- orems that make complex mathematical results within reach. In this paper, we propose a novel method called theoREm-from-prooF extrACTOR (REFACTOR) for training neural networks to mimic this ability in formal mathematical theorem proving. We show on a set of unseen proofs, REFACTOR is able to extract 19.6\% of the theorems that humans would use to write the proofs. When applying the model to the existing Metamath library, REFACTOR extracted 16 new theorems which are used frequently in the Metamath library, with an average usage of 733.5 times. With newly extracted theorems, we show that the existing proofs in the MetaMath database can be refactored to shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset is able to prove more test theorems.},
  eventtitle = {1st {{Mathematical Reasoning}} in {{General Artificial Intelligence Workshop}}, {{ICLR}} 2021.}
}

@article{powerCombiningMonadComonad2002,
  title = {Combining a Monad and a Comonad},
  author = {Power, John and Watanabe, Hiroshi},
  date = {2002-05},
  journaltitle = {Theoretical Computer Science},
  shortjournal = {Theoretical Computer Science},
  volume = {280},
  number = {1--2},
  pages = {137--162},
  issn = {03043975},
  doi = {10.1016/S0304-3975(01)00024-X},
  url = {https://linkinghub.elsevier.com/retrieve/pii/S030439750100024X},
  urldate = {2023-02-25},
  langid = {english},
  file = {/home/patrick/Zotero/storage/LYM2AP4G/Power and Watanabe - 2002 - Combining a monad and a comonad.pdf}
}

@article{powerFormalismSpecificationEssentiallyalgebraic1992,
  title = {A Formalism for the Specification of Essentially-Algebraic Structures in 2-Categories},
  author = {Power, A. J. and Wells, Charles},
  date = {1992-03},
  journaltitle = {Mathematical Structures in Computer Science},
  shortjournal = {Math. Struct. Comp. Sci.},
  volume = {2},
  number = {1},
  pages = {1--28},
  issn = {0960-1295, 1469-8072},
  doi = {10.1017/S0960129500001110},
  url = {https://www.cambridge.org/core/product/identifier/S0960129500001110/type/journal_article},
  urldate = {2025-06-29},
  abstract = {A type of higher-order two-dimensional sketch is defined which has models in suitable 2-categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of one-dimensional sketches. These sketches allow the specification of constructions in 2-categories such as weighted limits, as well as higher-order constructions such as exponential objects and subobject classifiers, that cannot be sketched by limits and colimits. These sketches are designed to be the basis of a category-based methodology for the description of functional programming languages, complete with rewrite rules giving the operational semantics, that is independent of the usual specification methods based on formal languages and symbolic logic. A definition of ‘path grammar’, generalizing the usual notion of grammar, is given as a step towards this goal.},
  langid = {english}
}

@book{quillenHomotopicalAlgebra1967,
  title = {Homotopical Algebra},
  author = {Quillen, Daniel G.},
  date = {1967},
  series = {Lecture Notes in Mathematics},
  number = {43},
  publisher = {Springer},
  location = {Berlin Heidelberg},
  isbn = {978-3-540-03914-3},
  langid = {english},
  note = {Mit Literaturverz},
  file = {/home/patrick/Zotero/storage/5C3I4QN6/Quillen - 1967 - Homotopical algebra.pdf}
}

@inproceedings{richardsonSystemDescriptionProof1998,
  title = {System {{Description}}: {{Proof Planning}} in {{Higher-Order Logic}} with {{LambdaClam}}},
  booktitle = {Automated Deduction, {{CADE-15}}: 15th {{International Conference}} on {{Automated Deduction}}, {{Lindau}}, {{Germany}}, {{July}} 5-10, 1998: Proceedings},
  author = {Richardson, Julian and Smaill, Alan and Green, Ian},
  date = {1998},
  pages = {130--133},
  publisher = {Springer},
  location = {Lindau, Germany},
  doi = {10.1007/BFb0054239},
  abstract = {Proof planning [4] is an approach to theorem proving which encodes heuristics for constructing mathematical proofs in a meta-theory of methods. The Clam system, developed at Edinburgh [3], has been used for several years to develop proof planning, in particular proof plans for induction. It has become clear that many of the theorem-proving tasks that we would like to perform are naturally higher-order. For example, an important technique called middle-out reasoning [6] uses meta-variables to stand for some unknown objects in a proof, to be instantiated as the proof proceeds. Domains such as the synthesis and  verification of software and hardware systems, and techniques such as proof critics [7], benefit greatly from such middle-out reasoning. Since in these domains the meta-variables often become instantiated with terms of function type, reasoning with them is naturally higher-order, and higher-order unification is a vital tool. One of our motivations for studying induction is that it is an important technique for reasoning about programs. Reasoning about programs (functions, predicates) is naturally higher-order, and although it is possible to reason about such objects in a first-order meta-theory, in order to do so we would have to modify our existing Clam methods to deal with proper treatment of A bindings, (3 reduction etc. The reasoning is much clearer if we use higher-order logic as the meta-theory. XClam is a higher-order prototype of Clam, written in XProlog, a higher- order version of Prolog. The meta-theory is based on higher-order logic, which simplifies reasoning about higher-order objects and allows many of the proof plans developed in Clam to be transferred to the higher-order setting without significant modifications. This is important because Clam constitutes a  significant knowledge base for (inductive) proof. The use of AProlog gives us a powerful meta-theory which allows methods to be written concisely and declaratively,  further enhancing one of the advantages of proof planning which is that it produces plans which are understandable to the human user.As well as being able to prove higher-order theorems which Clam cannot, LambdaClam is also capable of proving many first-order theorems.},
  eventtitle = {{{CADE-15}}: 15th {{International Conference}} on {{Automated Deduction}}},
  isbn = {978-3-540-64675-4}
}

@thesis{riehlAlgebraicModelStructures2011,
  type = {Monograph},
  title = {Algebraic {{Model Structures}}},
  author = {Riehl, Emily},
  date = {2011-06},
  institution = {The University of Chicago},
  location = {Chicago, Illinois},
  url = {https://math.jhu.edu/~eriehl/phdthesis.pdf},
  urldate = {2023-05-29},
  abstract = {Quillen’s model structures axiomatize a general framework for homotopy theory, providing tools to study the objects of a category up to some specified notion of weak equivalence. In a model cat- egory, the interactions between the weak equivalences and two additional classes of morphisms— the cofibrations and the fibrations—enable a concrete construction of the homotopy category; the category obtained by restricting to the fibrant-cofibrant objects and taking homotopy classes of maps is equivalent to the formal localization at the weak equivalences. Furthermore, model struc- tures enable one to perform constructions at the “point-set level”—i.e., in the original category, which typically has more limits and colimits than the homotopy category—that are homotopically meaningful in the sense that they agree with their derived functors. For these reasons, model categories have proliferated far beyond the original topological set- ting. But despite their popularity, ordinary model structures only provide a context for homotopy theory and don’t contribute directly to calculations. In this thesis we present a new, more rigid, algebraic extension of Quillen’s notion that has this calculational capacity because certain struc- tures previously only supposed to exist are now specified. This thesis lays the foundations for the theory of algebraic model structures, introducing a number of basic definitions, describing conditions that give rise to important examples, and discussing general features. Algebraic model structures, introduced in Part I of this thesis, provide a setting for homotopy theory in which the trappings of an ordinary model structure—the cofibrations, fibrations, trivial cofibrations, and trivial fibrations—can be thought of algebraically: as maps together with extra data witnessing their membership in the particular class. Each algebraic model structure deter- mines an underlying ordinary model category, in the sense of Quillen [Qui67], but one whose functorial factorizations have richer algebraic structure. Despite the fact that this new definition is much stricter than the original, an algebraic model structure exists whenever an ordinary model structure is cofibrantly generated. The abundance of such examples means that this theory offers a new perspective on classical model categories, which we believe will be of interest to experts, even if they see no immediate need for the algebraic structures we can guarantee. What does it mean to consider fibrations algebraically? A classical example is provided by the Hurewicz fibrations, which can be characterized as those maps of spaces that admit a path lifting viii function. Importantly, a path lifting function assigned to some map p is precisely an algebra structure for p with respect to a particular monad on the arrow category, whose objects are maps of spaces and whose morphisms are commutative squares [May75]. The monad is constructed from the Moore paths monad and describes, among other things, a functorial factorization of each arrow as a cofibration and homotopy equivalence followed by a fibration. The monad on the arrow category is the functor that replaces a map by a fibration, its right factor. Furthermore, the functor that sends a map to its left factor with respect to this functorial factorization, the trivial cofibration part, is itself a comonad on the arrow category. Its coalgebras are necessarily homotopy equivalences and Hurewicz cofibrations. Furthermore, the coalgebra structure assigned to a particular trivial cofibration can be used to construct a canonical solution to any lifting problem against a fibration equipped with a path lifting function. These are the general features of what it means to describe the trivial cofibrations and fibrations as “algebraic”: such maps are equipped with specified retractions to their left or right factors which can be used to solve all lifting problems. In an algebraic model structure, both functorial factorizations have this flavor: the right fac- tors are monads and the left factors are comonads. Algebras are necessarily fibrations and trivial fibrations, and coalgebras are necessarily trivial cofibrations and cofibrations, respectively. Addi- tionally, a natural comparison between the two functorial factorizations induces functors that map algebraic trivial cofibrations to algebraic cofibrations and algebraic trivial fibrations to algebraic trivial fibrations. These functors compatibly assign a canonical solution to any lifting problem between an algebraic trivial cofibration and an algebraic trivial fibration. The data of an algebraic model structure determines a fibrant replacement monad and cofi- brant replacement comonad; algebras and coalgebras are algebraic fibrant objects and algebraic cofibrant objects. Furthermore, the canonical solution to a particular lifting problem defines a distributive law of the monad over the comonad, which specifies the algebraic fibrant-cofibrant objects. Future work will explore the implications of the previously unnoticed fact that any cofi- brantly generated model category has a fibrant replacement monad and cofibrant replacement comonad, which, in particular, allows one to construct (co)simplicial resolutions using point-set derived functors. A paradigmatic cofibrantly generated algebraic model structure is Quillen’s original model structure on spaces, generated by the sets I = \{S n−1 → Dn\} and J = \{Dn → Dn × I\}. An algebraic fibration is a Serre fibration equipped with chosen lifts of cylinders in the base space ix extending specified disks in the total space. An algebraic trivial fibration is a map equipped with lifted contractions filling spheres in the total space which are contractible in the base. Such maps are necessarily both Serre fibrations and weak homotopy equivalences; that is, they are necessarily trivial fibrations in the underlying ordinary model structure. Conversely, all trivial fibrations admit some algebra structure: one need only make a choice among the various fillers for such spheres which necessarily exist. Indeed, whenever the algebraic model structure is cofibrantly generated, all fibrations and all trivial fibrations are algebraic. Interestingly, the dual statements do not hold: the cofibrations and trivial cofibrations need not admit coalgebra structures, even when the algebraic model structure is cofibrantly generated. Accordingly, we say a cofibration is cellular if it admits a coalgebra structure, that is, if there is some algebraic cofibration with this underlying map. The name is motivated by the most familiar example: a relative cell complex is a map of spaces, necessarily a cofibration, that can be described by repeatedly attaching cells to the domain. Such a description is called a cellular decomposition for the map and defines a coalgebra structure for the comonad. By convention, whenever two cells can be attached “at the same time” in a particular cellular decomposition, we do so, so that the filtration defined by the cellular decomposition will have fewer, in fact typically only countably many, stages. As is familiar for CW-complexes, a special case, the resulting coalgebra structures are not at all unique, even granting this convention. Not all cofibrations for this model structure are cellular. The best one can say is that the cofibrations are retracts of relative cell complexes, that is, retracts of cellular cofibrations. Analo- gously, in any algebraic model category, any cofibration is a retract of a cellular one. More specif- ically, any cofibration is a retract of a cofibration admitting a free coalgebra structure, namely, its left factor in the cofibration–trivial fibration factorization. For some algebraic model structures, the cellular cofibrations behave quite differently. For example, in Quillen’s model structure on simplicial sets, generated by the sphere and horn in- clusions, every cofibration is cellular and furthermore admits a unique coalgebra structure. Here the cofibrations are precisely the monomorphisms and the filtration defined by their cellular de- composition is always countable. The first step attaches all simplices whose boundary appears in the domain. In particular this includes all 0-simplices of the codomain. The second step attaches all simplices whose boundary is present at the end of stage one; in particular, this includes all 1-simplices. In this way, we see that the n-th simplicial set of the resulting filtration contains at least the (n − 1)-skeleton of the codomain. x When comparing algebraic model structures on different categories, cellularity is more than just a curiosity. A cellularity condition precisely characterizes algebraic Quillen adjunctions, a rigid analog of the classical notion. In an ordinary Quillen adjunction, the left adjoint preserves the (trivial) cofibrations and the right adjoint preserves the (trivial) fibrations. In an algebraic Quillen adjunction, a new definition introduced below, the left adjoint lifts to a functor between the algebraic (trivial) cofibrations and the right adjoint lifts to a functor between the algebraic (trivial) fibrations, and furthermore these lifts determine each other, in a sense that is rather del- icate to make precise. Modulo a compatibility condition which is not the main point, an adjunc- tion is an algebraic Quillen adjunction if and only if the images of the generating cofibrations and trivial cofibrations under the left adjoint are cellular with respect to the appropriate comonads. Furthermore, a choice of cell structures completely determines the lifted functors and hence the full algebraic Quillen adjunction. The geometric realization–total singular complex adjunction between simplicial sets and spaces is a member of a large class of examples. The geometric realizations of the generat- ing cofibrations are homeomorphic to the elements of the set I; we assign these maps the sim- plest possible I-cellular structures. Similarly, the geometric realizations of the horn inclusions are homeomorphic to the elements of J; again, we assign these maps the simplest J-cellular structures. In this case, the naturality condition, glossed over above, demands a good choice of I-cellular structures for the realizations of the horn inclusions: first attach the “missing face” to the geometrically realized horn to make a sphere, and then fill the sphere. The theme of cellularity, entirely present but not fully apparent to the author in Part I [Rie11], is unmistakable in Part II, which introduces monoidal algebraic model structures, algebraicizing the definition of [Hov99]. Extending the results for the single-variable case, algebraic Quillen two-variable adjunctions exist precisely when the pushout-products of the generating cofibrations and trivial cofibrations are cellular; furthermore, these cellular structures completely determine the algebraic Quillen two-variable adjunctions. The main technical work of Part II is to precisely state the definition of an algebraic Quillen two-variable adjunction and prove these theorems, which are much harder than the single-variable versions, but once this technical work is complete, the definition of a monoidal algebraic model structure is apparent. Monoidal model structures necessarily precede consideration of enriched ones but also inherit nearly all of their complexity, so the definition of an enriched algebraic model structure is also evident. However, we leave this topic for another paper where we have time to more fully consider examples. xi In order to state the definitions and prove the theorems appearing in this thesis, we had to develop a fair amount of pure category theory. The precise definition of an algebraic Quillen ad- junction proved particularly fruitful, requiring a new notion of morphism between the categorical components of an algebraic model structure. Our discovery of the correct notion was motivated by a desire to replicate the classical situation where a Quillen adjunction can be detected by con- sidering the left adjoint and the (trivial) cofibrations or the right adjoint and the (trivial) fibrations alone. Alternatively, these definitions can be intuited from a purely categorical lens. The compo- nents of an algebraic Quillen adjunction are lax morphisms of monads and colax morphisms of comonads related by the calculus of mates [KS74], which governs the interactions between the monads and comonads arising from the same functorial factorization. An alternate approach uses the fact that the (co)algebra structures assigned to a composable pair of (co)fibrations are themselves composable in such a way that the algebraic (co)fibrations become a double category; algebraic Quillen adjunctions consist of compatible lifted double functors. In fact, the main reason the proofs in Part II are much harder than the corresponding arguments in Part I is that the functors between arrow categories arising from a two-variable adjunction do not preserve composability of underlying maps, much less (co)algebras. Thus, in the two-variable case, we are forced to rely upon the mates approach, but even here the necessary category theory does not exist. To describe the correct correspondence between the three lifted functors of an algebraic two-variable adjunction, we introduce parameterized mates and prove a few fundamental lemmas. In this paper, we consider only two-variable adjunctions, the case of interest, but the same ideas extend to n-variable adjunctions and can be used to define the 2- cells of a category object in the category of multicategories of a particular sort. Of all the topics developed here, we believe this to be of greatest independent categorical interest.},
  langid = {english},
  pagetotal = {143}
}

@book{riehlCategoricalHomotopyTheory2014,
  title = {Categorical Homotopy Theory},
  author = {Riehl, Emily},
  date = {2014},
  series = {New Mathematical Monographs},
  number = {24},
  publisher = {Cambridge University Press},
  location = {New York, NY},
  isbn = {978-1-107-04845-4},
  pagetotal = {352},
  keywords = {Algebra Homological,Homotopy theory}
}

@thesis{rosoliniContinuityEffectivenessTopoi1986,
  title = {Continuity and Effectiveness in Topoi},
  author = {Rosolini, Giuseppe},
  date = {1986-03-28},
  institution = {University of Oxford},
  location = {Cambridge},
  url = {https://www.google.com/url?sa=i&rct=j&q=&esrc=s&source=web&cd=&cad=rja&uact=8&ved=0CDYQw7AJahcKEwiQ5LfyyM__AhUAAAAAHQAAAAAQAw&url=https%3A%2F%2Fwww.researchgate.net%2Fprofile%2FGiuseppe-Rosolini%2Fpublication%2F35103849_Continuity_and_effectiveness_in_topoi%2Flinks%2F57ef75b908ae886b89741067%2FContinuity-and-effectiveness-in-topoi.pdf&psig=AOvVaw3O9sW8L-06higPLGTvTyB8&ust=1687272199493497&opi=89978449},
  abstract = {The categorical approach to recursion theory has produced very interesting results in such areas as the study of higher-type structure [Hyl77b, Sco80a, LS83] (the last contains also references to earlier work) and the study of models of computation [Sco82, Plo85]. The theory concentrates on the idea of ”com- putation” but often discards ”effectiveness”, although this notion should be represented in the theory: any mechanizable computation is certainly effective. Consequently, it is also necessary to represent the possibility of failure: a computation may diverge on some input. Therefore, it seems to be an inescapable conclusion that the theory must include a notion of partiality. At the present time, the development of the categorical approach to effectiveness presents two major directions: one focuses on Erˇsov’s category of enumerated sets and the study of its full subcategories (cf. [Smy77, Vis80, LM84c]). The essential structure of effectivity is determined by the maps rather than by the objects: a map f : \{an\}n∈N {$>$} \{bn\}n∈N between two enumerated sets is a function between the indexed sets such that the equation f(an) = bg(n) holds for some recursive function g. Many elementary facts of recursion theory can be expressed as properties of particular objects of the category. But, in order to study particular structures, one often has to refer back to the set N of indices, resulting in a rather heavy use of notation, and the main effort in proofs is usually concentrated in showing that some constructed set is an enumerated set. The other approach rejects altogether the idea that objects have to be enumerated in order to be given some effective structure, and it insists instead on having effectiveness as an internal feature of the whole universe. Rather than structuring sets with enumerations in the classical universe, one considers sets in an intuitionistic universe where a property such as “all functions on the set of natural numbers are recursive” may hold. The first example of this idea is the realizability model of [Kle45] (cf. [Tro73, McC84]), but it found its category-theoretic setting in [Hyl82] where the effective topos F is introduced. The effective topos has many desirable properties: the functions on the natural numbers are all recursive (Church’s Thesis), and the ω-Axiom of Choice and Markov’s Principle hold. Also, the category of enumerated sets is fully embedded in the effective topos as is the category PER of partial equivalence relations on the applicative structure on N. Martin Hyland and Eugenio Moggi announced that the interrnal full subcategory on stable quotients on N (the internal version of PER) is closed under internal arbitrary limits, a result suggesting very interesting developments in the theory of polymorphic types. Concerning the abstract theory of partiality, categories of partial maps appeared as examples of monoidal categories which were iatroduced by [EK66], but the main interest of the theory concerned categories of modules over a ring, and no real development of a theory for partiality came at that time. Much later [PH86] reconsidered the problem. In a series of lectures in Siena in 1984, they presented dominical categories in order to give a basic category-theoretic setting for an abstract study of recursion theory. At the same time, Gordon Plotkin made explicit the reason why Scott-continuous functions between complete partial orders are partial: his method was simply to remove the bottom element (which represents the ”undefined” va]ue) from each complete partial order, and consider what is left of the continuons functions between them. A first acconnt of a general category-theoretic treatment of this idea was considered by [LM84a], who drew categorical intuitions from the work of DiPaola and Heller. We are convinced that in a treatment of computations it is convenient and instructive to have an intuitionist’s attitude. Support for this approach rests on many works on intuitionistic mathematics. The work of this thesis is particularly influenced by the approach advocated by Dana Scott and his 6 Introduction collaborators [Sco79, Sco80b, Fou80, Gra79, McC84, Hyl82]. Our approach makes strong use of topos theory, which we think is the best expression of the link between category theory and intuitionism. Cat- egory theory has to do with closure properties of families of maps and with the characterization of maps and spaces in terms of mapping properties. Definability of these map is often important. Intuitionistic logic treats existence in terms of explicit constructions; hence, definability is again important. The conservative translation of category theory into intuitionistic logic makes the harmony between these theories precise. As we remarked, intuitionistic logic has models in which maps on the natural numbers are always computable (again, this is a kind of definability), so we combine under one point of view both algebraic explicitness and computational notions. An important question that has to be answered concerns the treatment of partiality in an intuitionistic world. We found an answer when we proved a representation theorem for dominical categories: every dominical category is a full subcategory of a category of partial maps on a topos [Ros85]. One can paraphrase this result as follows: every dominical category is a category of sets and partial functions. In the proof of that result it became clear how an intuitionist could choose to define partial functions: select a subset Σ of the set Ω of truth-values such that the truth-value true ∈ Σ, and accept as partial functions those whose domains of definition are classified by Σ. By this we mean that a partial function ϕ : X ⇀ Y is accepted if and only if ∀x ∈ X.|x ∈ dom ϕ| ∈ Σ. In order to obtain a category of partial functions, Σ must satisfy the further condition that p ∈ Σ ∧ [p = true → q ∈ Σ] → (p ∧ q) ∈ Σ With a questionable choice of name, we call such an object a dominance, because it classifies the domains of the partial functions. A final word about specializing these considerations to the classical case: in the topos S of classical sets, the two possible choices for a dominance give rise eactly to the two categories of total functions and of partial functions on sets. The interesting choices of dominance are found in non-Boolean topoi. For instance, in the effective topos F we can consider the set of truth-values which answer a recursive question: Σ = \{p ∈ Ω : ∃f ∈ NN.p ↔ (∃z ∈ N.f(z) = O)\}. This is a dominance. In F, all functions on the natural numbers are recursive, and the request f(z) = O represents a generic recursive statement. (We first saw this definition in a lecture by Dana Scott in Pisa in the fall of 1983). We argue beginning in Chapter 5 that properties of Σ make the relation between continuity and effectiveness of functions apparent. We discuss the study of the known models for computation and elaborate on their mutual relationships, in order to discuss the usefulness of having a universal notion of ”recursively enumerable”. In Chapter 8 we gather ideas from the results we obtain about the models to explain a possible synthetic approach to the theory of computation. To sustain our arguments in favour of such an approach, we must first explain the elementary theory for partial maps. To the best of our knowledge, what we present is original, and we compare it to the literature already available. In particular, in the generality of our treatment, we can answer some open questions presented in [PH86]. We then continue by presenting the general theory of dominance. We do not wish to claim that this is the way it has to be done. But, it is certainly very simple; it includes all the other theories; it has straightforward applications to some important categories of partial maps. We already explained that we are convinced that the use of this notion when looking at the models considerably helps intuition. And there is a very clear sense in which a dominance gives rise to continuity of functionals. In Chapter 1 we review the logical expressive power in a topos and discuss connected problems in Grothendieck topoi. In Chapter 2 we introduce p-categories as an abstraction of categories of partial maps and prove a completeness result for these. We compare our definition to others from the literature, consider a few common constructions of category theory in the context of p-categories, and solve some problems posed in [PH86] about stability of ranges and coproducts.},
  langid = {english},
  pagetotal = {110}
}

@online{sealTensorsMonadsActions2013,
  title = {Tensors, Monads and Actions},
  author = {Seal, Gavin J.},
  date = {2013-06-25},
  eprint = {1205.0101},
  eprinttype = {arXiv},
  eprintclass = {math},
  url = {http://arxiv.org/abs/1205.0101},
  urldate = {2023-02-04},
  abstract = {We exhibit sufficient conditions for a monoidal monad T on a monoidal category C to induce a monoidal structure on the Eilenberg–Moore category CT that represents bimorphisms. The category of actions in CT is then shown to be monadic over the base category C.},
  langid = {english},
  pubstate = {prepublished},
  keywords = {18C20 18D10 18D35,Mathematics - Category Theory},
  note = {Comment: v4: Minor corrections; added dedication},
  file = {/home/patrick/Zotero/storage/E79FPQ3W/Seal - 2013 - Tensors, monads and actions.pdf}
}

@inproceedings{sejourneUnbalancedGromovWasserstein2021,
  title = {The Unbalanced Gromov Wasserstein Distance: {{Conic}} Formulation and Relaxation},
  booktitle = {Advances in Neural Information Processing Systems},
  author = {Sejourne, Thibault and Vialard, Francois-Xavier and Peyré, Gabriel},
  editor = {Ranzato, M. and Beygelzimer, A. and Dauphin, Y. and Liang, P.S. and Vaughan, J. Wortman},
  date = {2021},
  volume = {34},
  pages = {8766--8779},
  publisher = {Curran Associates, Inc.},
  url = {https://proceedings.neurips.cc/paper_files/paper/2021/file/4990974d150d0de5e6e15a1454fe6b0f-Paper.pdf}
}

@online{shulmanHomotopyLimitsColimits2009,
  title = {Homotopy Limits and Colimits and Enriched Homotopy Theory},
  author = {Shulman, Michael},
  date = {2009-06-30},
  eprint = {math/0610194},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/math/0610194},
  urldate = {2023-05-27},
  abstract = {Homotopy limits and colimits are homotopical replacements for the usual limits and colimits of category theory, which can be approached either using classical explicit constructions or the modern abstract machinery of derived functors. Our first goal in this paper is expository: we explain both approaches and a proof of their equivalence. Our second goal is to generalize this result to enriched categories and homotopy weighted limits, showing that the classical explicit constructions still give the right answer in the abstract sense. This result partially bridges the gap between classical homotopy theory and modern abstract homotopy theory. To do this we introduce a notion of "enriched homotopical categories", which are more general than enriched model categories, but are still a good place to do enriched homotopy theory. This demonstrates that the presence of enrichment often simplifies rather than complicates matters, and goes some way toward achieving a better understanding of "the role of homotopy in homotopy theory."},
  pubstate = {prepublished},
  keywords = {55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
  note = {Comment: 79 pages; minor errors corrected},
  file = {/home/patrick/Zotero/storage/9NPDULB6/Shulman - 2009 - Homotopy limits and colimits and enriched homotopy.pdf;/home/patrick/Zotero/storage/SKZZ74U8/0610194.html}
}

@article{sobocinskiBeingVanKampen2011,
  title = {Being {{Van Kampen}} Is a Universal Property},
  author = {Sobocinski, Pawel and Heindel, Tobias},
  date = {2011-04-01},
  journaltitle = {Logical Methods in Computer Science},
  volume = {Volume 7, Issue 1},
  pages = {701},
  issn = {1860-5974},
  doi = {10.2168/LMCS-7(1:14)2011},
  url = {https://lmcs.episciences.org/701},
  urldate = {2023-06-25},
  abstract = {Colimits that satisfy the Van Kampen condition have interesting exactness properties. We show that the elementary presentation of the Van Kampen condition is actually a characterisation of a universal property in the associated bicategory of spans. The main theorem states that Van Kampen cocones are precisely those diagrams in a category that induce bicolimit diagrams in its associated bicategory of spans, provided that the category has pullbacks and enough colimits.},
  langid = {english},
  file = {/home/patrick/Zotero/storage/2SUDZHBY/Sobocinski and Heindel - 2011 - Being Van Kampen is a universal property.pdf}
}

@online{spivakSlicingMonadsCategories,
  title = {Slicing up Monads on Categories with Pullbacks: What Are These Mysterious Zerosumfree Monads},
  author = {Spivak, David},
  url = {https://mathoverflow.net/q/339143},
  organization = {Mathoverflow}
}

@letter{trimbleBarConstructions1999,
  type = {Letter},
  title = {Bar {{Constructions}}},
  author = {Trimble, Todd},
  date = {1999-09-05},
  url = {https://math.ucr.edu/home/baez/trimble/bar.html},
  urldate = {2023-06-18},
  abstract = {In this section, we initially work over a base topos Set; all of our  constructions apply in a context where we work over a Grothendieck  topos E as base. Later in this section, we take E to be the topos  of Joyal species.  Classically, bar constructions have been used to build classifying  bundles, free resolutions for group cohomology, and similar constructs.  A common characteristic between these constructions is the production of  an acyclic algebraic structure (e.g., a contractible G-space EG, or  a free resolution of a G-module). We begin by formalizing this  characteristic in terms of a universal property for bar constructions.},
  langid = {english}
}

@thesis{whitesideRefactoringProofs2013,
  type = {Thesis or Dissertation},
  title = {Refactoring {{Proofs}}},
  author = {Whiteside, Iain},
  date = {2013-11-28},
  institution = {The University of Edinburgh},
  location = {Edinburgh, Scotland},
  url = {https://era.ed.ac.uk/handle/1842/7970},
  urldate = {2013-10-22},
  abstract = {Refactoring is an important Software Engineering technique for improving the structure of a program after it has been written. Refactorings improve the maintainability, readability, and design of a program without affecting its external behaviour. In analogy, this thesis introduces proof refactoring to make structured, semantics preserving changes to the proof documents constructed by interactive theorem provers as part of a formal proof development. In order to formally study proof refactoring, the first part of this thesis constructs a proof language framework, Hiscript. The Hiscript framework consists of a procedural tactic language, a declarative proof language, and a modular theory language. Each level of this framework is equipped with a formal semantics based on a hierarchical notion of proof trees. Furthermore, this framework is generic as it does not prescribe an underlying logical kernel. This part contributes an investigation of semantics for formal proof documents, which is proved to construct valid proofs. Moreover, in analogy with type-checking, static well-formedness checks of proof documents are separated from evaluation of the proof. Furthermore, a subset of the SSReflect language for Coq, called eSSence, is also encoded using hierarchical proofs. Both Hiscript and eSSence are shown to have language elements with a natural hierarchical representation. In the second part, proof refactoring is put on a formal footing with a definition using the Hiscript framework. Over thirty refactorings are formally specified and proved to preserve the semantics in a precise way for the Hiscript language, including traditional structural refactorings, such as rename item, and proof specific refactorings such as backwards proof to forwards proof and declarative to procedural. Finally, a concrete, generic refactoring framework, called Polar, is introduced. Polar is based on graph rewriting and has been implemented with over ten refactorings and for two proof languages, including Hiscript. Finally, the third part concludes with some wishes for the future.},
  langid = {english},
  pagetotal = {254}
}

@inproceedings{zomboriLearningComplexActions2020,
  title = {Learning {{Complex Actions}} from {{Proofs}} in {{Theorem Proving}}},
  booktitle = {5th {{Conference}} on {{Artificial Intelligence}} and {{Theorem Proving}}. {{AITP}} 2020},
  author = {Zombori, Zsolt and Urban, Josef},
  date = {2020},
  location = {Aussois, France},
  url = {http://aitp-conference.org/2020/abstract/paper_11.pdf},
  abstract = {We propose to develop procedures that extend simple theorem provers with complex actions that are the result of learning. Learning is based on traces of successful proof attempts: we will use inductive logic programming (ILP) [5] to learn Prolog programs that can reproduce (some repetitive parts of) the proofs found. Such programs are then incorporated into the next iteration of the prover as new actions, resulting in a hierarchy of more advanced provers.},
  eventtitle = {5th {{Conference}} on {{Artificial Intelligence}} and {{Theorem Proving}}. {{AITP}} 2020}
}

@inproceedings{zomboriPrologTechnologyReinforcement2020,
  title = {Prolog {{Technology Reinforcement Learning Prover}}},
  booktitle = {{{IJCAR}} 2020: {{Automated Reasoning}}},
  author = {Zombori, Zsolt and Urban, Josef and Brown, Chad E.},
  date = {2020},
  pages = {489--507},
  publisher = {Springer},
  location = {Paris, France},
  doi = {10.1007/978-3-030-51054-1_33},
  url = {https://link.springer.com/chapter/10.1007/978-3-030-51054-1_33#citeas},
  abstract = {We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.},
  eventtitle = {International {{Joint Conference}} on {{Automated Reasoning}}},
  isbn = {978-3-030-51053-4}
}