Invited speakers

The workshop will feature three invited talks:

• Anuj Dawar, University of Cambridge
• Nicola Gambino, University of Leeds
• Alexandra Silva, Radboud University Nijmegen

Anuj Dawar, Fixed-point Approximations of Graph Isomorphism

The problem of deciding if two graphs are isomorphic is a well-studied problem in computational complexity that is neither known to be in P nor known to be NP-complete. There are families of equivalence relations on graphs, which are known to over-approximate isomorphism, which are decidable in polynomial time. One such family, the Weifeiler-Lehman equivalence relations, has a number of equivalent characterisations arising in logic, algebra and combinatorics, and can be naturally described as the greatest fixed-points of natural refinement operators. In this talk review these various characterisations and examine refinements of the family of relations that are obtained by considering coherent algebras over finite fields.

This is joint work with Bjarki Holm.

Nicola Gambino, Cartesian closed bicategories.

It is well known that cartesian closed categories provide models for the simply-typed lambda calculus in which the beta and eta rules are valid as strict equalities. Moving from standard, 1-dimensional, category theory to 2-dimensional category theory, it is possible to formulate the notion of a cartesian closed bicategory, which gives us models where the beta and eta rules are interpreted as isomorphisms. The aim of this talk is to describe in elementary terms what cartesian closed bicategories are and present a new example which arises in the theory of operads.

This is based on joint work with André Joyal.

Alexandra Silva, Rational fixpoints in programming languages

Functional languages offer a high level of abstraction which results in elegant, easy to understand, programs. Central to the development of functional programming are inductive and coinductive types and associated programming constructs, such as pattern-matching. Whereas inductive types have a long tradition and are well supported in most languages, coinductive types are subject of more recent research and less mainstream.

In this talk we will discuss language constructs to enable the definition of recursive functions on regular coinductive types. We will present CoCaml, a functional programming language extending OCaml, where these language constructs have been implemented . We show a variety of examples, including operations on infinite lists, infinitary lambda-terms and p-adic numbers.