<div dir="ltr"><div class="gmail-ajy" tabindex="0">[Apologies for multiple copies]<br></div><br>Dear all,<br><br>Let me advertise our next ERATO MMSD project
<span class="gmail-m_6832220814482882016gmail-m_547872329642204051m_1674442457263079573gmail-il"><span class="gmail-m_6832220814482882016gmail-il"><span class="gmail-il">colloquium</span></span></span> 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.<br><br>Sincerely,<br>--<br>Natsuki Urabe<br><a href="mailto:urabenatsuki@is.s.u-tokyo.ac.jp" target="_blank">urabenatsuki@is.s.u-tokyo.ac.j<wbr>p</a><br>The University of Tokyo, ERATO MMSD<br><br>-----<br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" id="gmail-docs-internal-guid-05f1c6d9-0045-1079-f59c-d14c09b2fd6d"><span style="font-size:14pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"></span></p><span style="font-size:14pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Thu 30 November 2017, 16:30–18:45</span><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:8pt;font-family:Arial;color:rgb(255,0,0);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">ERATO MMSD Takebashi Site Common Room 3</span><span style="font-size:8pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"><br class="gmail-kix-line-break"></span><a href="http://group-mmm.org/eratommsd/access.html" style="text-decoration:none"><span style="font-size:8pt;font-family:Arial;color:rgb(17,85,204);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:underline;vertical-align:baseline">http://group-mmm.org/eratommsd/access.html</span></a></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:12pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">16:30-17:30</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Jérémy Dubut (NII), </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"> </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"><br class="gmail-kix-line-break"></span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Some thoughts on bisimilarity using open morphisms</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:Arial;color:rgb(102,102,102);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">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.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:Arial;color:rgb(102,102,102);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">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.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:12pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">17:45-18:45</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Akihisa Yamada (NII), </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline"> </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:rgb(255,255,255);font-weight:700;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">Mathematics for Complexity Analysis</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:Arial;color:rgb(102,102,102);background-color:rgb(255,255,255);font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline">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.</span></p></div>