MSCS is moving to continuous publishing.

We give a simple, direct, and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of automatic differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode AD.

The starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $\boldsymbol{\omega } \mathbf{Cpo}$-semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument.

The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$-cpos.

In this paper, we study the approximate minimization problem of weighted finite automata (WFAs): to compute the best possible approximation of a WFA given a bound on the number of states. By reformulating the problem in terms of Hankel matrices, we leverage classical results on the approximation of Hankel operators, namely the celebrated Adamyan-Arov-Krein (AAK) theory. We solve the optimal spectral-norm approximate minimization problem for irredundant WFAs with real weights, defined over a one-letter alphabet. We present a theoretical analysis based on AAK theory and bounds on the quality of the approximation in the spectral norm and $\ell ^2$ norm. Moreover, we provide a closed-form solution, and an algorithm, to compute the optimal approximation of a given size in polynomial time.

This article constructs the moduli stack of torsion-free $G$-jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$-topos equipped with any stable factorization systems.

In the intended applications of this theory, the factorization systems are given by the deRham-Stack construction. Homotopy type theory allows a formulation of this abstract theory with surprisingly low complexity. This is witnessed by the accompanying formalization of large parts of this work.

We present our library for universal algebra in the UniMath framework dealing with multi-sorted signatures, their algebras and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.