Browsing 2023 by Author "Lucatelli Nunes, Fernando"
Now showing items 1-5 of 5
-
Automatic Differentiation for ML-Familiy Languages: Correctness via Logical Relations
[OWP-2023-07] Lucatelli Nunes, Fernando; Vákár, Matthijs (Mathematisches Forschungsinstitut Oberwolfach, 2023-06-19) -
Cauchy Completeness, Lax Epimorphisms and Effective Descent for Split Fibrations
[OWP-2023-06] Lucatelli Nunes, Fernando; Prezado, Rui; Sousa, Lurdes (Mathematisches Forschungsinstitut Oberwolfach, 2023-06-19)For any suitable base category $\mathcal{V} $, we find that $\mathcal{V} $-fully faithful lax epimorphisms in $\mathcal{V} $-$\mathsf{Cat} $ are precisely those $\mathcal{V}$-functors $F \colon \mathcal{A} \to \mathcal{B}$ ... -
Lax Comma Categories of Ordered Sets
[OWP-2023-08] Clementino, Maria Manuel; Lucatelli Nunes, Fernando (Mathematisches Forschungsinstitut Oberwolfach, 2023-06-19)Let $\mathsf{Ord} $ be the category of (pre)ordered sets. Unlike $\mathsf{Ord}/X$, whose behaviour is well-known, not much can be found in the literature about the lax comma 2-category $\mathsf{Ord} //X$. In this paper ... -
Logical Relations for Partial Features and Automatic Differentiation Correctness
[OWP-2023-09] Lucatelli Nunes, Fernando; Vákár, Matthijs (Mathematisches Forschungsinstitut Oberwolfach, 2023-06-19)We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can ... -
Semantic Factorization and Descent
[OWP-2023-05] Lucatelli Nunes, Fernando (Mathematisches Forschungsinstitut Oberwolfach, 2023-06-19)Let $\mathbb{A}$ be a $2$-category with suitable opcomma objects and pushouts. We give a direct proof that, provided that the codensity monad of a morphism $p$ exists and is preserved by a suitable morphism, the factorization ...