[logic-ml] Project colloquium talk by Jérémy Dubut and Akihisa Yamada on 30 November

[urabenatsuki at is.s.u-tokyo.ac.jp]

[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 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20171128/4676f09d/attachment.html>