[Apologies for multiple copies]

Dear all,

Let me advertise our next ERATO MMSD project colloquium talk by Jérémy Dubut and Akihisa Yamada on 30th November, 16:30-. Please find the title and the abstract below. You are all invited.

Sincerely, -- Natsuki Urabe urabenatsuki@is.s.u-tokyo.ac.jp The University of Tokyo, ERATO MMSD

-----

Thu 30 November 2017, 16:30–18:45

ERATO MMSD Takebashi Site Common Room 3 http://group-mmm.org/eratommsd/access.html

16:30-17:30

Jérémy Dubut (NII), Some thoughts on bisimilarity using open morphisms

In this talk, I will present some work I have done on open morphisms during my PhD. I will start by giving an introduction on this categorical formalism from Joyal, et al.’s work on bisimilarity defined as the existence of a span of morphisms having some lifting properties with respect to “execution shapes”. I will show you examples, relational and logical characterisations for this bisimilarity.

Next, I would like to present two quite different aspects of this theory that I used during my PhD. First, a general framework, called the accessible categorical models, where the open morphisms formalism is particularly nice. This is a case where it is possible to define a nice notion of trees. In this framework, we show that bisimilarity can be precisely captured by the existence of some bisimulation relation on executions, but also that there is a fine notion of unfolding, which acts very similarly as a universal covering. Secondly, a particular case of the theory of Joyal et al.: the bisimilarity of diagrams, namely functors from a small category to a specified category of values. I will show you that this case is equivalent to the existence of a nice notion of bisimulations, which allows us to translate the problem of bisimilarity, to a problem of isomorphisms in the category A, which is useful for (un)decidability. I will finally show you how to translate the general setting of Joyal et al. where the category of paths is small into diagrams, and I will describe the relation between the different bisimilarities involved.

17:45-18:45

Akihisa Yamada (NII),

Mathematics for Complexity Analysis

IsaFoR is a library of Isabelle-formalized theorems for validating program analyzers, originally on term rewriting. My previous work was to extend the library for more practical programing languages and also to enrich the library with deep results from mathematics. In this talk, I will explain how complexity analysis leads us to formalizing algebraic numbers, the Berlekamp factorization, Jordan normal forms, and the Perron-Frobenius theorem.