<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>