Programme

• Julian Salamanca, 13:30 – 14:15

• Renato Neves, 14:30 – 15:15

• Henning Basold, 15:30 – 16:15

Equations and Coequations for Weighted Automata

Julian Salamanca ¹

We study weighted automata from both an algebraic and a coalgebraic perspective. In particular, we consider equations and coequations for weighted automata. We prove a duality result that relates sets of equations (congruences) with (certain) subsets of coequations. As a consequence, we obtain two equivalent but complementary ways to define classes of weighted automata. We show that this duality cannot be generalized to linear congruences in general but we obtain partial results when weights are from a field.

This is joint work with Marcello Bonsangue and Jan Rutten.

Towards a calculus of hybrid components

Renato Neves ²

Despite us rapidly moving towards a reality where software is prevalently intertwined with continuous processes, the design of such systems remains a difficult challenge, mainly due to the need to accommodate both discrete and continuous behaviour in a single framework.

One starting point to address this issue is to find a suitable monad that captures continuous behaviour as a computational effect, similarly to what has been done for probabilistic behaviour and non—determinism. Such an approach puts (Kleisli) composition in a central place, and favours a component calculus for whatever systems the monad collects.

This talk introduces a monad for continuous behaviour and discusses the relevance of the corresponding Kleisli category as a suitable environment to study the effects of continuity over composition. The monad paves the way for a calculus of continuous components, and may play a key rôle in a calculus for hybrid ones.

Dependent Inductive and Coinductive Types via Dialgebras in Fibrations

Henning Basold ^{3 1}

In this talk, I will establish the necessary structure to give semantics to dependent inductive and coinductive types, and want to speculate about possible extensions.

It is well-known that dependent type theories à la Martin-Löf can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how these data type definitions correspond to initial and final dialgebras for these functors. This description can be seen as a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. I also show how dependent data types correspond to algebras and coalgebras to attain constructions of these types, and I will investigate induction and coinduction principles for data types.

Finally, if time permits, I would like to speculate on how to extend this work to, what I call, Higher Coinductive Types that are supposed to capture subobjects. These form the dual to Higher Inductive Types, used in Homotopy Type Theory to, among other things, capture quotients.