Joint Seminar on Mathematical Structures in Computer Science

Coalgebras provide a natural setting for describing (potentially) infinite behaviour of systems and recurrences via local observations. The theory of coalgebra comprises abstract reasoning principles for the equivalence of system behaviour, abstract composition and transformation operations, coalgebraic logic as a generalisation of modal logic, and tools for analysing long-term behaviour.

In this talk, I will provide an introduction to the field of coalgebra and its techniques, and show that it provides a fundamental understanding of many recursive structures in mathematics and computer science. We will see in depth the usefulness of coalgebraic proof techniques to reason about smooth functions, and sketch out a broad range of examples from probability theory, logic, dynamical systems and programming languages. Moreover, we will illustrate the power of abstraction through a generalisation of the existence theorem of stationary distributions for Markov chains to general coalgebras. Finally, I will highlight a few ongoing research directions.

Coalgebras provide a natural setting for describing (potentially) infinite behaviour of systems and recurrences via local observations. The theory of coalgebra comprises abstract reasoning principles for the equivalence of system behaviour, abstract composition and transformation operations, coalgebraic logic as a generalisation of modal logic, and tools for analysing long-term behaviour.

In this talk, I will provide an introduction to the field of coalgebra and its techniques, and show that it provides a fundamental understanding of many recursive structures in mathematics and computer science. We will see in depth the usefulness of coalgebraic proof techniques to reason about smooth functions, and sketch out a broad range of examples from probability theory, logic, dynamical systems and programming languages. Moreover, we will illustrate the power of abstraction through a generalisation of the existence theorem of stationary distributions for Markov chains to general coalgebras. Finally, I will highlight a few ongoing research directions.

Coinduction in R-modules, for R a commutative ring, is useful in e.g., describing the behaviour of linear weighted automata. In this talk, we describe the construction and properties of final coalgebras with a focus on R-modules. First we sketch the relevant background information on convergence ordinals for finitary functors in locally presentable categories. We then give an example of a binary intersection preserving, finitary functor on the category of abelian groups that fails to converge in ω+ω steps, thus settling a question of Adámek, Milius, and Moss. We relate this to the failure of the Artinian property for ℤ and show that all finitary functors on RMod preserving countable intersections and a generalised notion of monomorphism converge in ω(n + 2) steps, where n is the Krull dimension of R.

Time permitting, we may also explain how conditions for behavioural equivalence to imply bisimulation may be given in terms of the Ext¹ functor from homological algebra. This is joint work with Henning Basold and Chase Ford.

Coalgebras provide a natural setting for describing (potentially) infinite behaviour of systems and recurrences via local observations. The theory of coalgebra comprises abstract reasoning principles for the equivalence of system behaviour, abstract composition and transformation operations, coalgebraic logic as a generalisation of modal logic, and tools for analysing long-term behaviour.

In this talk, I will provide an introduction to the field of coalgebra and its techniques, and show that it provides a fundamental understanding of many recursive structures in mathematics and computer science. We will see in depth the usefulness of coalgebraic proof techniques to reason about smooth functions, and sketch out a broad range of examples from probability theory, logic, dynamical systems and programming languages. Moreover, we will illustrate the power of abstraction through a generalisation of the existence theorem of stationary distributions for Markov chains to general coalgebras. Finally, I will highlight a few ongoing research directions.

Quantales provide a common generalisation of algebraic logic (lattices, Boolean or Heyting algebras, etc.) and of quantitative logic. Typical examples of quantales are the frame of open sets of a topological space [3], the Lawvere quantale of extended real numbers [3,4], and probability distribution functions [1,2]. I will give a brief introduction to quantales. Then I show that a commutative-unital quantale Q induces a fibration Q-Pred of Q-valued predicates, which admits an interpretation of linear first-order logic. These results have been formalized in Rocq

In this talk, we present a formal theory of coalgebras, formulated internally in a double category. Our primary goal is to instantiate this to the enriched setting, providing a general theory of enriched coalgebras. To this end, we characterise categories of coalgebras abstractly as universal objects in double categories, adapting Kelly’s 2-categorical notion of inserters to double categories by instantiating them in the underlying morphism 2-category. A major advantage of this double-categorical formulation is that it allows us to prove that coalgebra objects inherit weighted colimits from the base category, without the assumption of cartesian closedness. Our main result is that coalgebra objects are given functorially by a limit-preserving double functor, which comes equipped with a natural projection which creates weighted colimits. We will apply these results by instantiating them to several enriched settings, study coalgebras in the double category of fibrations, and work towards a framework for coalgebraic logic internal to double categories.