~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[en:seminaires:types:index|Type theory and realisability]]\\
Tuesday July 18, 2023, 2PM, Salle 147 (bâtiment Olympe de Gouge)\\
**Paige North** (Utrecht University) //Coinductive control of inductive data types//
<button type="link" size="xs" collapse="b17-3386">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3386" collapsed="true">
<well size="sm">
In classical programming language theory, characterizing data types as initial
algebras of an endofunctor that represents a specification of the data types is
an important tool. In this work, we observe that the category of algebras of
such an endofunctor is often enriched in its category of coalgebras. This
enrichment carries strictly more information than the traditional, unenriched
category. For example, when considering the endofunctor whose initial algebra
is the natural numbers, we find that the enrichment encodes a notion of
`partial' homomorphism, while the unenriched category encodes only `total'
homomorphisms. We can also leverage this extra information to generalize the
notion of initial algebras, following the theory of weighted limits.
</well>
</collapse>