Programme

• Fabio Zanasi, 13:30 – 14:15

• Helle Hvid Hansen, 14:30 – 15:15

• Henning Basold, 15:30 – 16:15

Axiomatising linear systems: the case of signal flow graphs

Fabio Zanasi ¹

We present by generators and equations the theory IH whose free model is the category of linear subspaces over a field k. Terms of IH are string diagrams which, for different choices of k, express different kinds of networks and graphical formalisms used by scientists in various fields, such as categorical quantum mechanics, concurrency and control theory. The equations of IH arise by distributive laws between PROPs of Hopf algebras, from which the name interacting Hopf algebras stems. As main application, we use IH to axiomatise a formal semantics of signal processing circuits, for which we study full abstraction and realisability. Our analysis suggests a reflection about the role of causality in the semantics of computing devices.

This is a joint work with Filippo Bonchi and Pawel Sobocinski.

Coalgebraic Dynamic Logics: Basic Completeness Results

Helle Hvid Hansen ^{2 3}

I will present a coalgebraic generalisation of Fischer and Ladner’s Propositional Dynamic Logic (PDL) and Parikh’s Game Logic (GL). The basic observation is that programs (or games) are coalgebras for a monad T, the program constructs arise from Kleisli composition and algebraic structure on T, and the axioms of these logics correspond to certain compatibility requirements between the modalities and this structure. This setup allows us to prove two general completeness results: strong completeness without iteration, and (weak) completeness with iteration and “negation-free” pointwise operations.

(Joint work with Clemens Kupke and Raul Leal.)

Coinductive Techniques for Proving Productivity

Henning Basold ^{4 3}

In this talk, I will show how systems of mixed inductive-coinductive equations can be proved well-defined by means of coinduction. The notion of well-definedness combines termination for inductive equations and productivity for coinductive equations. Combined with up-to techniques, which take the operational aspect of equations into account, we arrive at a powerful proof principle for well-definedness. To make this proof principle useful also in the presence of (higher-order) function definitions, we need to enhance it further by deriving up-to techniques from already defined programs. I will demonstrate this on an example.

This is joint work with Helle H. Hansen.