Skip to content
Snippets Groups Projects
Select Git revision
  • ff24b519d5cbc56b3b78c69687e19ba8a57eafe4
  • master default
  • object
  • develop protected
  • private_algos
  • cuisine
  • SMOTE
  • revert-76c4cca5
  • archive protected
  • no_graphviz
  • 0.0.2
  • 0.0.1
12 results

multiclass.doctree

Blame
  • index.html 79.87 KiB
    <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
        "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
    
    <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en">
      <head>
        <meta http-equiv="content-type" content="application/xhtml+xml; charset=utf-8" />
        <meta name="author" content="Uli Fahrenberg" />
        <link rel="stylesheet" type="text/css" href="CSS/site.css" title="RAMICS stylesheet" />
        <link rel="stylesheet" type="text/css" media="print" href="CSS/print.css" title="RAMICS print stylesheet" />
    
        <title>RAMICS 2021</title>
    
        <script>
          MathJax = {
          tex: {
          inlineMath: [['$', '$']]
          },
          svg: {
          fontCache: 'global'
          }
          };
        </script>
        <script type="text/javascript" id="MathJax-script" async
    	    src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
        </script>
        <script language="javascript">
          function toggleDiv(divid){
    	if(document.getElementById(divid).style.display == 'none'){
    	  document.getElementById(divid).style.display = 'inline';
    	}else{
    	  document.getElementById(divid).style.display = 'none';
    	}}
        </script>
      </head>
    
      <body>
    
    <!-- ###### Header ###### -->
    
        <div id="header">
          <span class="headerTitle">
    	<a href="index.html">Relational and Algebraic Methods in Computer Science (RAMICS 2021)</a></span>
        </div>
    
        <!-- ###### Side Boxes ###### -->
    
        <div class="sideBox LHS">
          <div>Contents</div>
    	<a href="index.html">Home</a>
    	<a href="#program">Program</a> 
    	<a href="#invited">Invited speakers</a>
    	<!-- <a href="#accepted">Accepted papers</a> -->
    	<a href="#registration"><font color="red">Registration</font></a>
    <!--	<a href="#invited">Invited talks</a> -->
    <!--	<a href="ramics2021-flyer.pdf">Flyer</a> -->
    	<a href="#venue">Venue</a>
    <!--	<a href="#cfp">Call for papers</a> -->
    	<a href="#cfsc"><font color="red">Call for short contributions</font></a>
    	<a href="#dates">Important dates</a>
    <!--	<a href="#social">Social event</a> -->
    	<a href="#sponsors">Sponsors</a>
    	<a href="mailto:ramics2021@easychair.org">Contact</a>
        </div>
    
        <div class="sideBox LHS">
          <div>Invited Speakers</div>
    <!--
          <a href="index.html">To be announced</a>
          <a href="https://www.irif.fr/~petrisan/">Daniela Petrisan, France</a> -->
    <a href='https://scholar.google.com.ar/citations?user=ChPjZ80AAAAJ&hl=es'>Marcelo Frias, Argentina</a>
    <a href='https://www.uni-due.de/theoinf/people/koenig.php'>Barbara König,
      Germany</a>
    <!--
    <a href='http://people.stfx.ca/wmaccaul/'>Wendy MacCaull, Canada</a>
    -->
    <a href='http://intsys.msu.ru/en/staff/zhuk/'>Dmitriy  Zhuk,
      Russia</a>
    
        </div>
    
        <!--
        <div class="sideBox LHS">
          <div>Accepted papers</div>
          <a href="accepted.html">List of accepted papers</a>
        </div>
        -->
    
        
        <div class="sideBox LHS">
          <div>Program Committee</div>
    <a href='https://www.uva.nl/en/profile/a/f/b.afshari/b.afshari.html'>Bahareh Afshari, The Netherlands</a>
    <a href='https://wwwtcs.inf.tu-dresden.de/~baier/'>Christel Baier, Germany</a>
    <a href='https://www.math.tu-dresden.de/~bodirsky/'>Manuel Bodirsky, Germany</a>
    <a href='https://scholar.google.com/citations?user=-uYpcPwAAAAJ&hl=en'>Ignacio Fábregas, Spain</a>
    <a href='http://www.lix.polytechnique.fr/Labo/Ulrich.Fahrenberg/'>Uli
      Fahrenberg, France (co-chair)</a>
    <a href='https://www.sci.kagoshima-u.ac.jp/furusawa/'>Hitoshi Furusawa, Japan</a>
    <a href='https://math.unice.fr/~mgehrke/'>Mai Gehrke, France (co-chair)</a>
    <a href='https://homes.di.unimi.it/ghilardi/'>Silvio Ghilardi, Italy</a>
    <a href='http://rolandglueck.de/'>Roland Glueck, Germany</a>
    <a href='https://www.csse.canterbury.ac.nz/walter.guttmann/'>Walter
      Guttmann, New Zealand</a>
    <a href='http://www.cs.ucl.ac.uk/staff/robin_hirsch/'>Robin Hirsch, UK</a>
    <a href='http://www.hoefner-online.de/'>Peter Höfner, Australia</a>
    <a href='https://scholar.google.com/citations?user=rWJLBq8AAAAJ&hl=en'>Ali Jaoua, Qatar</a>
    <a href='http://www1.chapman.edu/~jipsen/'>Peter Jipsen, USA</a>
    <a href='http://sjcjoosten.nl/'>Sebastiaan Joosten, USA</a>
    <a href='http://lkovacs.com/'>Laura Kovacz, Austria</a>
    <a href='https://www8.cs.fau.de/wp-content/uploads/staff/litak/'>Tadeusz Litak, Germany</a>
    <a href='https://faculty.sites.iastate.edu/maddux/'>Roger Maddux, USA</a>
    <a href='http://www.lix.polytechnique.fr/Labo/Dale.Miller/'>Dale Miller, France</a>
    <a href='https://www.h-brs.de/en/inf/prof-dr-martin-e-mueller'>Martin Mueller, Germany</a>
    <a href='https://www.irif.fr/~petrisan/'>Daniela Petrisan, France</a>
    <a href='http://perso.ens-lyon.fr/damien.pous/'>Damien Pous, France</a>
    <!--<a href='http://www0.cs.ucl.ac.uk/staff/D.Pym/'>David Pym, UK</a> -->
    <!-- <a href='https://msadrzadeh.com/'>Mehrnoosh Sadrzadeh, UK</a> -->
    <a href='http://pageperso.lif.univ-mrs.fr/~luigi.santocanale/'>Luigi
      Santocanale, France (co-chair)</a>
    <a href='http://staffwww.dcs.shef.ac.uk/people/G.Struth/'>Georg Struth, UK</a>
    <a href='https://www.samvangool.net/'>Sam van Gool, France</a>
    <a href='http://www.cosc.brocku.ca/~mwinter/'>Michael Winter, Canada (co-chair)</a>
        </div>
    
        <div class="sideBox LHS">
          <div>Organizing Committee</div>
          <a href="http://www.lix.polytechnique.fr/Labo/Ulrich.Fahrenberg/">Uli
    	Fahrenberg</a>
          <a href="https://math.unice.fr/~mgehrke/">Mai Gehrke</a>
          <a href="http://pageperso.lif.univ-mrs.fr/~luigi.santocanale/">Luigi
    	Santocanale</a>
          <a href="http://www.cosc.brocku.ca/~mwinter/">Michael Winter</a>
        </div>
    
        <div class="sideBox LHS">
          <div>Steering Committee</div>
          <a href="http://www.rpe.informatik.uni-kiel.de/en">Rudolf Berghammer</a>
          <a href="http://www.lix.polytechnique.fr/Labo/Ulrich.Fahrenberg/">Uli
    	Fahrenberg</a>
          <a href="http://www.csse.canterbury.ac.nz/walter.guttmann/">Walter
    	Guttmann</a>
          <a href="http://www.hoefner-online.de/">Peter Höfner</a>
          <a href="">Ali Jaoua</a>
          <a href="http://www1.chapman.edu/~jipsen/">Peter Jipsen</a>
          <a href="http://www.cosc.brocku.ca/~mwinter/">Michael Winter (chair)</a>
        </div>
    
    <!-- ###### Body Text ###### -->
    
        <div id="bodyText">
    
          <h1 id="intconf">
    	19th International Conference on<br />
    	Relational and Algebraic Methods in Computer Science<br />
    	RAMICS 2021
          </h1>
    
    <!--      
          <center>
    	<img class="noprint" src="lakeX3.jpg" title="École
    	polytechnique" alt="View on École polytechnique from the lake"
    	/>
          </center>
          -->
          
          <p>RAMICS 2021 will take place
    	at <a href="https://www.cirm-math.com/">CIRM</a> close to
    	Marseille from <strong>2 to 5 November</strong> 2021. 
          </p>
    
    
    <!--      
          <center>
    	<a href="ramics19-poster.pdf">Download conference poster</a> (or
    	in <a href="ramics19-poster-a4.pdf">A4 format</a>)
          </center>
    
          <center>
    	Download <a href="dhs2019-program.pdf">program</a> (or as
    	a <a href="dhs2019-program-book.pdf">booklet</a>)
          </center>
    -->
    
    <!--      <h3 id="news"><font color="red">News</font></h3> -->
    
          <p>Since 1994, the RAMiCS conference series has been the main
    	venue for research on relation algebras, Kleene algebras and
    	similar algebraic formalisms, and their applications as
    	conceptual and methodological tools in computer science and
    	beyond.</p>
          
          <p>Theoretical aspects include semigroups, residuated lattices,
    	semirings, Kleene algebras, relation algebras, quantales and
    	other algebras; their connections with program logics and
    	other logics; their use in the theories of automata,
    	concurrency, formal languages, games, networks and programming
    	languages; the development of algebraic, algorithmic,
    	category-theoretic, coalgebraic and proof-theoretic methods
    	for these theories; their formalisation with theorem
    	provers.</p>
    
    <!--     
          <img src="statueX.jpg" alt="Statue commemorating the role of
          students of École polytechnique in the defence of Paris in 1814"
          title="Statue at École polytechnique" style="float:right;
          margin-top:0px; margin-bottom:0px; margin-left:20px;
          margin-right:0px" />
          -->
          
          <p>Applications include tools and techniques for program
    	correctness, specification and verification; quantitative and
    	qualitative models and semantics of computing systems and
    	processes; algorithm design, automated reasoning, network
    	protocol analysis, social choice, optimisation and
    	control.</p>
    
    <!--      <h3 id="invited">Invited Talks</h3> -->
          <h3 id="invited">Invited Speakers</h3>
    
          <p>
          <!--To be announced.-->
          <ul>
    	<li><a href='https://scholar.google.com.ar/citations?user=ChPjZ80AAAAJ&hl=es'>Marcelo Frias, Argentina</a></li>
    	<li><a href='https://www.uni-due.de/theoinf/people/koenig.php'>Barbara König, Germany</a></li>
    	<li><a href='http://intsys.msu.ru/en/staff/zhuk/'>Dmitriy  Zhuk, Russia</a></li>
          </ul>
          </p>
    
          <h3 id="accepted">Accepted papers</h3>
          <p>
    	List of <a href="accepted.html">accepted papers</a>.
          </p>
    
          <h3 id="registration">Registration</h3>
          <p>
    	Please register using
    	the <a href="http://www.cirm-math.fr/preRegistration/index.php?EX=menu0&id_renc=2398">CIRM's
    	pre-registration page</a>.
          </p>
    
          <h3 id="venue">Venue</h3>
    
          <p>RAMICS 2021 will take place
    	at <a href="https://www.cirm-math.com/">CIRM</a>,
    	the <i>Centre International de Rencontres Mathématiques</i>,
    	at Luminy campus close to Marseille and on the border of the
    	<a href="https://www.marseille-tourisme.com/en/discover-marseille/highlights/nature/the-calanques/">Calanques</a>
    	National Park.
    	<!--
          </p>
          
          <p>
    	--> There will be no inscriptions fees to the conference, you
    	will only need to
    	care of <a href="https://www.cirm-math.com/prices.html">lodging
    	and catering expenses at CIRM</a>.  A limited number of
    	grants, covering both lodging and catering, are being sponsored by
    	<a href="https://www.cirm-math.com/">CIRM</a> and
    	the <a href="https://labex-archimede.univ-amu.fr/">Archimède
    	Institute</a>.
          </p>
    
    
          <center>
    	<iframe width="560" height="315"
    	src="https://www.youtube-nocookie.com/embed/9hLYT7W9V4w"
    	frameborder="0" allow="accelerometer; autoplay;
    	clipboard-write; encrypted-media; gyroscope;
    	picture-in-picture" allowfullscreen></iframe>
          </center>
    
          <h3>Access to virtual room</h3>
    
          <p>
    	Will be available from
    	the <a href="https://conferences.cirm-math.fr/2398.html">CIRM
    	web page of this conference.</a>
          </p>
    
          <h3>Proceedings</h3>
    
          <p>
    	The RAMiCS-19 proceedings are available
    	at <a href="https://link.springer.com/book/10.1007/978-3-030-88701-8">the
    	  Springer website</a>.
    	<!--
    	and
    	at <a href="http://link.springer.com/openurl.asp?genre=issue&issn=0302-9743&volume=12062">SpringerLink</a>. -->
          </p>
    
          
    
    
          <h3 id="program">Program</h3>
          
    
          All times in CET; click on time to convert to other time zones. 
    
          Speakers are underlined, click on titles to see abstracts.
    
          The program is also available as a <a href="program.pdf">pdf
    	file</a>.
    
          
          <!-- Insert program here -->
    
          
    <table padding='0px', cellpadding='5px', width='99%'>
    <tr ><th colspan="3", style="padding:10pt">Monday November 1, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-01T18:30:00">19:30</a></td><td colspan="2", style="padding:5pt"><b >Dinner</b></td></tr>
    <tr ><th colspan="3", style="padding:10pt">Tuesday November 2, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T06:00:00">7:00</a></td><td colspan="2", style="padding:5pt"><b >Breakfast</b></td></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T07:50:00">8:50</a></td><td colspan="2", style="padding:5pt"><b >Opening</b></td></tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right">9:00</td>
    <td></td>
    <td align="left">Session 1. Chair <i>Roland Glück</i></td>
    </tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T08:00:00">9:00</a></td>
    <td align="left"><i ><u >Christophe Lucas</u> and Matteo Mio</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T1')">Free Modal Riesz Spaces are Archimedean: a Syntactic Proof</a>
    <div style="display:none", id="T1"><br /><br />We prove, using syntactical proof–theoretic methods, that free modal Riesz spaces are Archimedean. Modal Riesz spaces are Riesz spaces (real vector lattices) endowed with a positive linear 1–decreasing operator, and have found application in the development of probabilistic temporal logics in the field of formal verification. All our results have been formalised using the Coq proof assistant.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T08:30:00">9:30</a></td>
    <td align="left"><i ><u >Wesley Fussner</u> and William Zuluaga Botero</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T2')">Some modal and temporal translations of generalized basic logic</a>
    <div style="display:none", id="T2"><br /><br />We introduce a family of modal expansions of Łukasiewicz logic that are designed to accommodate modal translations of generalized basic logic (as formulated with exchange, weakening, and falsum). We further exhibit algebraic semantics for each logic in this family, in particular showing that all of them are algebraizable in the sense of Blok and Pigozzi. Using this algebraization result, we establish that each of the introduced modal Łukasiewicz logics has a local deduction detachment theorem. By applying Jipsen and Montagna's poset product construction, we give two translations of generalized basic logic with exchange, weakening, and falsum in the style of the celebrated Gödel-McKinsey-Tarski translation. The first of these interprets generalized basic logic in a modal Łukasiewicz logic in the spirit of classical S4, whereas the second interprets generalized basic logic in a temporal variant of the latter.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T09:00:00">10:00</a></td>
    <td align="left"><i >Willem Conradie, Valentin Goranko and <u >Peter Jipsen</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T3')">Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm PEARL</a>
    <div style="display:none", id="T3"><br /><br />The theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, have recently been extended to the language RL of relevance logics with respect to their standard Routley-Meyer relational semantics. As a result, the non-deterministic algorithmic procedure PEARL (acronym for 'Propositional variables Elimination Algorithm for Relevance Logic') has been developed for computing first-order equivalents of formulae of the language RL in terms of that semantics. PEARL is an adaptation of the previously developed algorithmic procedures SQEMA (for normal modal logics) and ALBA (for distributive and non-distributive modal logics). It succeeds on all inductive formulae in the language RL, in particular on all previously studied classes of Sahlqvist formulae for relevance logic. In the present work, we re-interpret the algorithm PEARL from an algebraic perspective with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras. This enables us to complete the part of the Sahlqvist theorem still outstanding from the previous work, namely the fact that all inductive RL formulas are canonical, i.e., are preserved under canonical extensions of relevant algebras. Via the discrete duality between perfect relevant algebras and Routley-Meyer frames, this establishes the fact that all inductive RL formulas axiomatise logics which are complete with respect to first-order definable classes of Routley-Meyer frames. This generalizes the "canonicity via correspondence" result in [Urquhart, 1996] for (what we can now recognise as) a certain special subclass of Sahlqvist formulas in the "groupoid" sublanguage of RL where fusion is the only connective. By extending RL with a unary connective for converse and adding the necessary axioms, our results can also be applied to bunched implication algebras and relation algebras. We then present an optimised and deterministic version of PEARL, which we have recently implemented in Python and applied to verify the first-order equivalents of a number of important axioms for relevance logics known from the literature, as well as on several new types of formulae. In the paper, we report on the implementation and on some testing results.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T09:30:00">10:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right">11:00</td>
    <td></td>
    <td align="left">Session 2. Chair <i>Sam van Gool</i></td>
    </tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T10:00:00">11:00</a></td>
    <td align="left"><i >Frank Valencia, <u >Sergio Ramírez</u>, Santiago Quintero and Carlos Pinzón</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T4')">Computing Aggregated Knowledge as the Greatest Lower Bound of Knowledge</a>
    <div style="display:none", id="T4"><br /><br />In economics and multi-agent systems, \emph{aggregated (or distributed) knowledge} of a group is the knowledge of someone who knows exactly what every member of the group knows. This notion can be used to analyse the implications of the knowledge of a community if they were to combine their knowledge. In this paper we use fundamental tools from the theory of distributive lattice to characterize and compute aggregate knowledge.We prove that for distributive lattices of size $n$, (1) the meet of join-endomorphisms can be computed in time $O(n)$. Previous upper bound was $O(n^2)$. We show that (2) aggregated knowledge of given group can be viewed as the meet of the knowledge of each member of the group. We also show that for state sets of size $n$, (3) aggregated knowledge can be computed in time $O(n^2)$ in the general case and (4) for $S5$ knowledge (or \emph{Aumman structures}), it can be computed in time $O(n\alpha(n))$ where $\alpha(n)$ is the inverse of the Ackermann function.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T10:30:00">11:30</a></td>
    <td align="left"><i >Cameron Calk, Uli Fahrenberg, Christian Johansen, <u>Georg Struth</u> and Krzysztof Ziemiański</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T5')">lr-Multisemigroups, Modal Quantales and the Origin of Locality</a>
    <div style="display:none", id="T5"><br /><br />We introduce lr-multisemigroups as duals of modal quantales and study correspondences between equations in these multisemigroups and the domain and codomain axioms of modal quantales. Our results yield construction principles for modal powerset quantales that cover a wide range of models and applications.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T11:00:00">12:00</a></td>
    <td align="left"><i ><u >Jérémie Marquès</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T6')">Polyadic spaces and profinite monoids</a>
    <div style="display:none", id="T6"><br /><br />Hyperdoctrines are an algebraization of first-order logic introduced by Lawvere. Joyal proposed to apply pointwise Stone duality to get what he called a polyadic space. He also proposed the idea of Stirling kernels of a polyadic space that we generalize here in order to adapt the notion of polyadic space to certain special classes of first-order theories. We will see how these ideas can be applied to establish a correspondence between equidivisible profinite semigroups with open multiplication and some first-order theories with a linear order symbol.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T11:30:00">12:30</a></td><td colspan="2", style="padding:5pt"><b >Lunch</b></td></tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right">14:00</td>
    <td></td>
    <td align="left">Session 3. Chair <i>Silvio Ghilardi</i></td>
    </tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T13:00:00">14:00</a></td>
    <td align="left"><i ><u >Dmitriy Zhuk</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T7')"><b >Quantified Constraint Satisfaction Problem: towards the classification of complexity (invited talk)</b></a>
    <div style="display:none", id="T7"><br /><br />The Quantified Constraint Satisfaction Problem (QCSP) is 
    the generalization of the Constraint Satisfaction problem (CSP) where 
    we are allowed to use 
    both existential and universal quantifiers. 
    Formally, the QCSP over a constraint language $\Gamma$ is 
    the problem 
    to evaluate 
    a sentence of the form $$\forall x_1 \exists y_1\forall x_2 \exists y_2 \dots \forall x_n \exists y_n \ (R_{1}(\dots)\wedge\dots
    \wedge R_{s}(\dots)),$$ 
    where $R_1,\dots,R_s$ are  relations from $\Gamma$.
    While CSP remains in NP for any $\Gamma$, QCSP$(\Gamma)$ can be PSpace-hard, as witnessed by Quantified 3-Satisfiability or Quantified Graph 3-Colouring. 
    For many years there was a hope that 
    for any constraint language the QCSP is either in P, 
    NP-complete, or PSpace-complete. Moreover, 
    a very simple conjecture describing the complexity 
    of the QCSP was suggested by Hubie Chen.
    However, 
    in 2018 together with Mirek Ol\u{s}\'ak and Barnaby Martin 
    we discovered constraint languages 
    for which the QCSP is coNP-complete, DP-complete, 
    and even $\Theta_{2}^{P}$-complete, which refutes
    the Chen conjecture.
    Despite the fact that we described the complexity for 
    each constraint language on a 3-element domain with constants, 
    we did not hope to obtain a complete classification. 
    
    This year I obtained several results 
    that make me believe that 
    such a classification is closer than it seems. 
    First, I obtained an elementary proof of the 
    PGP reduction, which allows to reduce the QCSP to the CSP.
    Second, I showed that there is a gap between 
    $\Pi_{2}^{P}$ and PSpace, and found a criterion for the 
    QCSP to be PSpace-hard.
    In the talk I will discuss the above and some other results.
    </div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T14:00:00">15:00</a></td>
    <td align="left"><i >Natanael Alpay, Peter Jipsen and <u >Melissa Sugimoto</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T8')">Unary-determined distributive l-magmas and bunched implication algebras</a>
    <div style="display:none", id="T8"><br /><br />A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge,\vee,\cdot)$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is \emph{unary-determined} if $x\cdot y=(x\top\wedge y)\vee(x\wedge \top y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $p,q$. We obtain simple conditions on $p,q$ such that $x\cdot y=(px\wedge y)\vee(x\wedge qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T14:30:00">15:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right">16:00</td>
    <td></td>
    <td align="left">Session 4. Chair <i>Uli Fahrenberg</i></td>
    </tr>
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T15:00:00">16:00</a></td>
    <td align="left"><i ><u >Wolfgang Poiger</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T9')">Many-valued modal logic over a semi-primal algebra (short talk)</a>
    <div style="display:none", id="T9"><br /><br />Since semi-primal algebras behave similarly to the two-element Boolean algebra, it makes sense to consider many-valued logic over a semi-primal algebra of truth values. Our interest lies in modal extensions of such logics. Through their respective dual categories we explore the relationship between the variety HSP(L) generated by a semi-primal algebra L and the variety BA of Boolean algebras. As an example, we utilize this relationship to prove a many-valued analogue of the Goldblatt-Thomason Theorem. Furthermore, we discuss the underlying coalgebraic picture and discuss how one may lift results from the classical case to the many-valued case.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T15:20:00">16:20</a></td>
    <td align="left"><i >Stefano Aguzzoli and <u >Matteo Bianchi</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T10')">Amalgamation property for varieties of BL-algebras generated by one chain with finitely many components</a>
    <div style="display:none", id="T10"><br /><br />BL-algebras are the algebraic semantics for Hajek's Basic Logic BL, the logic of all continuous t-norms and their residua. In this paper we study the amalgamation property for the varieties of BL-algebras generated by one BL-chain with finitely many components.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T15:50:00">16:50</a></td>
    <td align="left"><i ><u >Claudia Muresan</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T11')">Subreducts and Subvarieties of PBZ*–lattices (short talk)</a>
    <div style="display:none", id="T11"><br /><br />PBZ∗–lattices are the paraorthomodular Brouwer–Zadeh lattices whose pairs of elements with their Kleene complements satisfy the Strong De Morgan condition; more precisely, they are bounded lattices endowed with two unary operations:
    • an involution ·′, called Kleene complement, which satisfies the Kleene condition: x ∧ x′ ≤ y ∨ y′, as well as paraorthomodularity ((x ≤ y & x′ ∧ y ≈ 0) → x ≈ y, which becomes an equational condition under the other axioms of PBZ∗–lattices) – so the bounded involution lattice reduct of any PBZ∗–lattice is a paraorthomodular pseudo–Kleene algebra, but it turns out that not all paraorthomodular pseudo–Kleene algebras are reducts of PBZ∗–lattices,
    • and the Brouwer complement, which reverses order, is smaller than the Kleene complement, which it only equals on the sharp elements (i.e. the elements having their Kleene complement as a bounded lattice complement), and satisfies only one of the De Morgan laws, along with condition (∗), which is obtained from the other De Morgan law (called Strong De Morgan) by replacing one of the variables with the Kleene complement of the other.
    These algebras arise in the study of Quantum Logics and they include orthomodular lattices with an
    extended signature (with the two complements coinciding), as well as antiortholattices (whose Brouwer
    complements are trivial). From the other abstractions of the sets of quantum events within the unsharp
    approach to quantum theory, PBZ∗–lattices present the advantage of forming a variety, that we denote ∗
    by PBZL .
    Antiortholattices turn out to have directly irreducible lattice reducts and, under distributivity, no
    nontrivial elements with bounded lattice complements.
    We establish a lattice isomorphism between the lattice of subvarieties of the variety SAOL generated
    by the antiortholattices with the Strong De Morgan property and the ordinal sum of the three–element chain with the lattice of subvarieties of the variety PKA of pseudo–Kleene algebras, which also gives us axiomatizations for all subvarieties of SAOL from those of the subvarieties of PKA.
    The form of this lattice isomorphism proves that the variety PKA is generated by the class of the bounded involution lattice reducts of the members of SAOL, thus also by the quasivariety of paraortho- modular pseudo–Kleene algebras and by the class of the bounded involution lattice reducts of the members of PBZL∗, which also shows that neither of these classes is a variety.
    We obtain an infinite ascending chain of varieties of distributive PBZ∗–lattices, which, along with the well–known infinite ascending chain of varieties of modular ortholattices and its image through the lattice isomorphism mentioned above, give us an infinity of pairwise disjoint infinite ascending chains of varieties of PBZ∗–lattices.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T16:10:00">17:10</a></td>
    <td align="left"><i ><u >Khyodeno Mozhui</u> and K. V. Krishna</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T12')">On the Representation Number of Bipartite Graphs (short talk)</a>
    <div style="display:none", id="T12"><br /><br />A word-representable graph is a simple graph G which can be represented by a word w over the vertices of G such that any two vertices are adjacent in G if and only if they alternate in w. It is known that the class of comparability graphs – the graphs which admit a transi- tive orientation – is precisely the class of graphs that can be represented by a concatenation of permutations of vertices. The class of bipartite graphs is a subclass of comparability graphs. While it is an open prob- lem to determine the representation number of comparability graphs, it was conjectured that the representation number of bipartite graphs on n vertices is at most n/4. In this paper, we propose a polynomial time relabeling algorithm to produce a word representing a given bipartite graph which is a concatenation of permutations of the graph’s vertices. Thus we obtain an upper bound for the representation number of bipar- tite graphs, which in turn gives us an upper bound for the dimension of the posets corresponding to bipartite graphs.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-02T18:30:00">19:30</a></td><td colspan="2", style="padding:5pt"><b >Dinner</b></td></tr>
    <tr ><th colspan="3", style="padding:10pt">Wednesday November 3, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T06:00:00">7:00</a></td><td colspan="2", style="padding:5pt"><b >Breakfast</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T08:00:00">9:00</a></td>
    <td align="left"><i ><u >Callum Bannister</u>, Peter Höfner and Georg Struth</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T13')">Effect Algebras, Girard Quantales and Complementation in Separation Logic</a>
    <div style="display:none", id="T13"><br /><br />We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. This shows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T08:30:00">9:30</a></td>
    <td align="left"><i ><u >Luigi Santocanale</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T14')">Skew metrics valued in Sugihara semigroups</a>
    <div style="display:none", id="T14"><br /><br />We consider skew metrics (equivalently, transitive relations that are tournaments, linear orderings) valued in Sugihara semigroups on autodual chains. We prove that, for odd chains and chains without a unit, skew metrics classify certain tree-like structures that we call perfect augmented plane towers. When the chain is finite and has cardinality $2K+1$, skew metrics on a set $X$ give rise to plane rooted trees of height $K$ whose frontier is a linear preorder of $X$.Any linear ordering on $X$ gives rise to an ordering on the set of its skew metrics valued on an arbitrary involutive residuated lattice $Q$. If $Q$ satisfies the mix rule, then this poset is most often a lattice. We study this lattice for $X = \{1,\ldots ,n\}$ and $Q$ the Sugihara monoid on the chain of cardinality $2K+1$. We give a combinatorial model of this lattice by describing its covers as moves on a appropriate space of words coding perfect augmented plane trees. Using the combinatorial model, we develop enumerative considerations on this lattice.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T09:00:00">10:00</a></td>
    <td align="left"><i >George Metcalfe, Sam van Gool, Adrien Guatto and <u >Simon Santschi</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T15')">Time Warps, from Algebra to Algorithms</a>
    <div style="display:none", id="T15"><br /><br />Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T09:30:00">10:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T10:00:00">11:00</a></td>
    <td align="left"><i ><u >Roland Glück</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T16')">Isolated Sublattices and their Application to Counting Closure Operators</a>
    <div style="display:none", id="T16"><br /><br />This paper is dedicated to the investigation of the interplay between isolated sublattices and closure operators.Isolated sublattices are a special kind of sublattices which can serve to diminuish the number of elements of a lattice by means of a quotient lattice.At the same time, there are simple formulae for the relationship between the number of closure operators in the original lattice and its quotient.This connection can be used to derive an algorithm for counting closure operators, provided the lattice contains suitable isolated sublattices.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T10:30:00">11:30</a></td>
    <td align="left"><i ><u >Chad Nester</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T17')">A Variety Theorem for Relational Universal Algebra</a>
    <div style="display:none", id="T17"><br /><br />We consider an analogue of universal algebra in which generating symbols are interpreted as relations. We prove a variety theorem for these relational algebraic theories, in which we find that their categories of models are precisely the definable categories. The syntax of our relational algebraic theories is string-diagrammatic, and can be seen as an extension of the usual term syntax for algebraic theories.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T11:00:00">12:00</a></td>
    <td align="left"><i ><u >Cameron Calk</u>, Philippe Malbos and Eric Goubault</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T18')">Abstract Strategies and Coherence</a>
    <div style="display:none", id="T18"><br /><br />Normalisation strategies give a categorical interpretation of the notion of contracting homotopies via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, globular 2-Kleene algebras provide a formal setting for reasoning about coherence proofs in abstract rewriting systems. In this work, we formalise the notion of normalisation strategy in this setting. In such structures, normalisation strategies allow us to prove a formal coherence theorem via convergent abstract rewriting.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T11:30:00">12:30</a></td><td colspan="2", style="padding:5pt"><b >Lunch</b></td></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T12:30:00">13:30</a></td><td colspan="2", style="padding:5pt"><b >Business meeting</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T13:30:00">14:30</a></td>
    <td align="left"><i ><u >Marcelo Frias</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T19')"><b >Relational Tight Field Bounds for Distributed Analysis of Programs (invited talk)</b></a>
    <div style="display:none", id="T19"><br /><br />Relational tight field bounds are an abstraction of the
    semantics of data structures. In the presence of appropriate
    symmetry-breaking predicates, these bounds can be computed
    automatically and allow to dramatically speed up bug-finding using
    SAT-solving. In this lecture, after giving an introduction to tight
    field bounds and symmetry-breaking predicates, I will present a
    general technique for distributing program analyses. As examples, I
    will show how the technique allows one to distribute SAT-based
    bug-finding as well as symbolic execution over
    complex data types.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T14:30:00">15:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T15:00:00">16:00</a></td>
    <td align="left"><i ><u >Michael Winter</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T20')">Change of Base using Arrow Categories</a>
    <div style="display:none", id="T20"><br /><br />Arrow categories establish a suitable framework to reason about L-fuzzy relation abstractly. For each arrow category we can identify the Heyting algebra L that is used as the lattice of membership or truth values by the relations of the category. Therefore, arrow categories model the fixed-base approach to L-fuzziness, i.e., all relations of the given arrow category use the same membership values. In this paper we are interested in the process of changing the base, i.e., an operation that allows to switch from an L1-fuzzy relation to an L2-fuzzy relation by replacing all membership values from L1 by values from L2 . We will define and investigate this change of base between two abstract arrow categories for which component-wise reasoning cannot be performed.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T15:30:00">16:30</a></td>
    <td align="left"><i >George Addison, Sajal Saha, and <u >Michael Winter</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T21')">L-fuzzy Concept Analysis using Arrow Categories (short talk)</a>
    <div style="display:none", id="T21"><br /><br />The purpose of this paper is to investigate topics in fuzzy concept analysis using the theory of arrow categories. Our approach deals with the origi- nal, fuzzy data using fuzzy subsets in order to obtain a notion of fuzzy concepts, fuzzy concept lattices, and fuzzy association rules. Our approach is general in the sense that we only require a complete Heyting algebra as the lattice of truth values instead of the unit interval r0, 1s or a substructure thereof. In addition, our approach differs from most approaches in the literature, which usually first apply some kind of defuzzyfication, e.g., α-cuts, and then apply concept analysis in the classical (crisp) sense.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T15:50:00">16:50</a></td>
    <td align="left"><i ><u >Alexandre Fernandez</u>, Luidnel Maignan and Antoine Spicher</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T22')">Accretive Computation of Global Transformations</a>
    <div style="display:none", id="T22"><br /><br />Global transformations form a categorical framework adapting graph transformations to describe fully synchronous rule systems on a given data structure. In this work we focus on data structures that can be captured as presheaves (like sets, graphs or Petri nets) and study the computational aspects of such synchronous rule systems. To obtain an online algorithm, a complete study of the sub-steps within each synchronous step is done at the semantic level. This leads to the definition of accretive rule systems and a local criterion to characterize these systems. Finally an online computation algorithm for theses systems is given.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T16:20:00">17:20</a></td>
    <td align="left"><i ><u >Ralph Sarkis</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T23')">Quotienting a Monad via Projective Algebras (short talk)</a>
    <div style="display:none", id="T23"><br /><br />Quotient types are quite common in mathematics but they are rather difficult to implement in a programming language. For instance, one can easily define the type of pairs of integers $\mathsf{Int}\times \mathsf{Int}$, but in order to define the type of rational numbers, one needs to quotient $\mathsf{Int}\times \mathsf{Int}$ by the relation $(p,q) \sim (r,s) \Leftrightarrow ps = rq$, which is easier said than done. In the framework of monadic programming, datatypes are free algebras for a monad. Not all algebras for a monad are free, but they are all quotients of free algebras. An algebra for a monad is said to be \emph{projective} if it is both a quotient and a subalgebra of a free algebra. We show that a natural family of projective algebras can be seen as algebras for a quotient monad. In other words, when a quotienting operation is nice enough that 1) the resulting algebra is a subalgebra of the free algebra and 2) it satisfies some naturality condition, then we obtain a monad that models the quotient type.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T16:40:00">17:40</a></td>
    <td align="left"><i ><u >Cédric de Lacroix</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T24')">Generalizing Girard quantale in a symmetric closed monoidal category (short talk)</a>
    <div style="display:none", id="T24"><br /><br />The category of complete lattices and join-preserving maps is known to be star-autonomous and the semigroup of this category are called quan- tales. A Frobenius quantale is usually defined as a quantale with a du- alizing element. If this element is also cyclic, the quantale is called a Girard quantale and it can interpret the non-commutative linear logic. Two properties have motivated this work. First, the canonical quantale of endomorphism of a complete lattice is a Girard quantale if and only if this lattice is completely distributive. Secondly, completely distributive lattices have a categorical characterization: they are exactly the nuclear objects – i.e the mix arrow is an isomorphism – of the category of sup lattices. The aim of this work was to find out the kind of semigroup (we simply called them Girard semigroup) that generalize Girard quantale. With the right definition in hand we wanted to verify if the following con- jecture is satisfied: given a symetric closed monoidal category, the internal hom of an object with itself is a Girard semigroup if and only if this object is a nuclear object of the category – that is if the generalization of the above property is still true. We used a - slightly - more general definition of Frobenius and Girard quantales which led to a suitable definition of Frobenius and Girard semigroups in any symetric closed category. In this work we found several properties of these new structures and we proved that if an object is nuclear then the internal hom of this object with it- self has a structure of Girard semigroup. The converse implication of the conjecture is still to be proved.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T18:30:00">19:30</a></td><td colspan="2", style="padding:5pt"><b >Dinner</b></td></tr>
    <tr ><th colspan="3", style="padding:10pt">Thursday November 4, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T06:00:00">7:00</a></td><td colspan="2", style="padding:5pt"><b >Breakfast</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T08:00:00">9:00</a></td>
    <td align="left"><i ><u >Bernhard Möller</u>, Peter O'Hearn and Tony Hoare</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T25')">On Algebra of Program Correctness and Incorrectness</a>
    <div style="display:none", id="T25"><br /><br />Variations on the notion of Kleene algebra have been used to provide foundations of reasoning about programs, for instance by showing how Hoare Logic (HL) can be represented in algebra. This line of work has focussed on program correctness,i.e., proving the absence of bugs. Recently, Incorrectness Logic (IL) has been advanced as a reasoning formalism for the dual problem: proving the presence of bugs. IL is intended to underpin the use of logic in program testing and static bug finding. In this paper we describe an extension of Kleene algebra, an algebra with backwards diamond operators and countable joins for tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. In addition to embedding IL, the algebra retains the ability to embed HL, and to make connections between IL and HL specifications: In this sense, it unifies correctness and incorrectness reasoning in one formalism.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T08:30:00">9:30</a></td>
    <td align="left"><i ><u >Walter Guttmann</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T26')">Second-Order Properties of Undirected Graphs</a>
    <div style="display:none", id="T26"><br /><br />We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T09:00:00">10:00</a></td>
    <td align="left"><i >Walter Guttmann and <u >Nicolas Robinson-O'Brien</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T27')">Relation-algebraic Verification of Borůvka's Minimum Spanning Tree Algorithm</a>
    <div style="display:none", id="T27"><br /><br />Previous work introduced a relation-algebraic framework for reasoning about weighted-graph algorithms. We use this framework to prove partial correctness of Borůvka's minimum spanning tree algorithm. This is the first formal proof of correctness for this algorithm. We also discuss new abstractions that make it easier to reason about weighted graphs.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T09:30:00">10:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T10:00:00">11:00</a></td>
    <td align="left"><i ><u >Rudolf Berghammer</u> and Mitja Kulczynski</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T28')">Experimental Investigation of Sufficient Criteria for Relations to Have Kernels</a>
    <div style="display:none", id="T28"><br /><br />We investigate four well-known criteria for the existence of kernels in directed graphs/relations which efficiently can be tested, namely to be irreflexive and symmetric, to be progressively finite, to be bipartite, and to satisfy Richardson's criterion. The numerical data, obtained by the evaluation of relation-algebraic problem specifications by means of RelView, show that even the most general of them is very far away from a characterisation of the class of directed graphs having kernels.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T10:30:00">11:30</a></td>
    <td align="left"><i ><u >Rudolf Berghammer</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T29')">Relational Computation of Sets of Relations</a>
    <div style="display:none", id="T29"><br /><br />We present a technique for the relational computation of sets RR of relations. It is based on a specification of a relation R to belong to RR by means of an inclusion $s \subseteq t$, where s and t are relation-algebraic expressions constructed from a vector model of R in a specific way. To get the inclusion, we apply properties of a mapping that transforms relations into their vectors models and, if necessary, point-wise reasoning. The desired computation of RR via a relation-algebraic expression r is then immediately obtained from the inclusion using a result published in the proceedings of MPC 2015. Compared with a direct development of r from a logical specification of R to belong to RR, the proposed technique is much more simple. We demonstrate its use by some classes of specific relations and also show some applications.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T11:00:00">12:00</a></td>
    <td align="left"><i ><u >Kangfeng Ye</u>, Simon Foster and Jim Woodcock</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T30')">Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving</a>
    <div style="display:none", id="T30"><br /><br />Semantics for nondeterministic probabilistic sequential programs is well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised its proof, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP, an Isabelle/HOL based proof framework for UTP, enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an example to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T11:30:00">12:30</a></td><td colspan="2", style="padding:5pt"><b >Lunch</b></td></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T13:00:00">14:00</a></td><td colspan="2", style="padding:5pt"><b >Free afternoon</b></td></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-04T18:30:00">19:30</a></td><td colspan="2", style="padding:5pt"><b >Dinner</b></td></tr>
    <tr ><th colspan="3", style="padding:10pt">Friday November 5, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T06:00:00">7:00</a></td><td colspan="2", style="padding:5pt"><b >Breakfast</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T08:00:00">9:00</a></td>
    <td align="left"><i >Agi Kurucz, Vladislav Ryzhikov, <u >Yury Savateev</u> and Michael Zakharyaschev</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T31')">Deciding FO-definability of Regular Languages</a>
    <div style="display:none", id="T31"><br /><br />We prove that, similarly to known PSpace-completeness of recognising FO(<)-definability of the language L(A) of a DFA A, deciding both FO(<,C)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC0 and ACC0) are PSpace-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by `localisable' properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSpace-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T08:30:00">9:30</a></td>
    <td align="left"><i >Damien Pous, Jurriaan Rot and <u >Jana Wagemaker</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T32')">On Tools for Completeness of Kleene Algebra with Hypotheses</a>
    <div style="display:none", id="T32"><br /><br />In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by reproving completeness of KAT and treat several other examples.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T09:00:00">10:00</a></td>
    <td align="left"><i ><u >Jas Šemrl</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T33')">Domain Range Semigroups and Finite Representations</a>
    <div style="display:none", id="T33"><br /><br />Relational semigroups with domain and range are a useful tool for modelling nondeterministic programs. We prove that the representation class R(D,R,*) is not finitely axiomatisable, answering [JM19, Question 4.9]. We show that any signature containing D, R, ˘, ; but not - or · has the finite representation property, an extension of the result for ordered domain algebras {0,1,D,R,≤,1',˘,;} [EH13]. We survey the results in the area of the finite representation property and raise a number of open questions.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T09:30:00">10:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T10:00:00">11:00</a></td>
    <td align="left"><i ><u >Amina Doumane</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T34')">The class of representable semilattice-ordered monoids is not a variety</a>
    <div style="display:none", id="T34"><br /><br />We show a necessary and a sufficient condition for a quasi-variety to be a variety. Using this, we show that the quasi-variety of representable semilattice-ordered monoids is not a variety.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T10:30:00">11:30</a></td>
    <td align="left"><i ><u >Stepan Kuznetsov</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T35')">Relational Models for the Lambek calculus with Intersection and Unit</a>
    <div style="display:none", id="T35"><br /><br />We consider the Lambek calculus extended with intersection (meet) operation. For its variant which does not allow empty antecedents, Andreka and Mikulas (1994) prove strong completeness w.r.t.\ relational models (R-models). Without the antecedent non-emptiness restriction, however, only weak completeness w.r.t.\ R-models (so-called square ones) holds (Mikulas 2015). Our goals are as follows. First, we extend the calculus with the unit constant, introduce a class of non-standard R-models for it, and prove completeness. This gives a simpler proof of Mikulas' result. Second, we prove that strong completeness does not hold. Third, we extend our weak completeness proof to the infinitary setting, to so-called iterative divisions (Kleene star under division).</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T11:00:00">12:00</a></td>
    <td align="left"><i ><u >Matthias Naaf</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T36')">Computing Least and Greatest Fixed Points in Absorptive Semirings</a>
    <div style="display:none", id="T36"><br /><br />We present two methods to algorithmically compute both least and greatest solutions of polynomial equation systems over absorptive semirings (with certain completeness and continuity assumptions), such as the tropical semiring. Both methods require a polynomial number of semiring operations, including semiring addition, multiplication and an infinitary power operation.Our main result is a closed-form solution for least and greatest fixed points based on the fixed-point iteration. The proof builds on the notion of (possibly infinite) derivation trees; a careful analysis of the shape of these trees allows us to collapse the fixed-point iteration to a linear number of steps. The second method is an iterative symbolic computation in the semiring of generalized absorptive polynomials, largely based on results on Kleene algebras.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T11:30:00">12:30</a></td><td colspan="2", style="padding:5pt"><b >Lunch</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T13:00:00">14:00</a></td>
    <td align="left"><i ><u >Barbara König</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T37')"><b >Fixpoint Games (invited talk)</b></a>
    <div style="display:none", id="T37"><br /><br />Solving fixpoint equations is a recurring problem in several domains:
    the result of a dataflow analysis can be characterized as either a
    least or greatest fixpoint. It is well-known that bisimilarity - the
    largest bisimulation - admits a characterization as a greatest
    fixpoint and furthermore mu-calculus model-checking requires to solve
    systems of nested fixpoint equations.
    
    Often, these fixpoint equations or equation systems are defined over
    powerset lattices, however in several applications - such as
    lattice-valued or real-valued mu-calculi - the lattice under
    consideration is not a powerset.
    
    Hence we extend the notion of fixpoint games (or unfolding games,
    introduced by Venema) to games for equation systems over more general
    lattices. In particular continuous lattices admit a very elegant
    characterization of the solution.
    
    We will also describe how to define progress measures which describe
    winning strategies for the existential players and explain how
    abstractions and up-to functions can be integrated into the
    framework. 
    
    (Joint work with Paolo Baldan, Tommaso Padoan, Christina
    Mika-Michalski)
    .</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T14:00:00">15:00</a></td>
    <td align="left"><i ><u >Michael Winter</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T38')">Relational Sums and Splittings in Categories of L-fuzzy Relations</a>
    <div style="display:none", id="T38"><br /><br />Dedekind categories and similar structures provide a suitable framework to reason about binary relations in an abstract setting. Arrow categories extend this theory by certain operations and axioms so that additional aspects of L-fuzzy relations become expressible. In particular, arrow categories allow to identify crisp relations among all relations. On the other hand, the new operations and axioms in arrow categories force the category to be uniform, i.e., to be within a particular subclass of Dedekind categories. As an extension, arrow categories inherit constructions from Dedekind categories such as the definition of relational sums and splittings. However, these constructions are usually modified in arrow categories by requiring that certain relations are additionally crisp. This additional crispness requirement and the fact that the category is uniform raises a general question about these constructions in arrow categories. When can we guarantee the existence of the construction with and without the additional requirement of crispness in the given arrow category or or an extension thereof? This paper provides a complete answer to this complex question for the two constructions mentioned.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T14:30:00">15:30</a></td><td colspan="2", style="padding:5pt"><b >Coffee break</b></td></tr>
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T15:00:00">16:00</a></td>
    <td align="left"><i ><u >Michael Winter</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T39')">FuReM - A System for Visualization and Manipulation of L-Fuzzy Relations (short talk)</a>
    <div style="display:none", id="T39"><br /><br />In this presentation we will introduce the FuReM (Fuzzy Relation Manipulator) sys- tem. This system allows to visualize and manipulate so-called L-fuzzy relations similar to the RelView system.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T15:20:00">16:20</a></td>
    <td align="left"><i ><u >Jas Šemrl</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T40')">Finite Representation Property for Relation Algebra Reducts (short talk)</a>
    <div style="display:none", id="T40"><br /><br />Membership in the Class of Representable Tarskian Relation Algebra in undecid- able. However, dropping some operations to obtain a reduct language may introduce some more favourable properties. The Finite Representation Property (FRP) is a great example of good algebraic behaviour. A signature is said to have the FRP if every rep- resentable finite structure in that signature can be represented over a finite base set. Some positive implications of the FRP for a signature include the decidability of mem- bership in the representation class for finite structures, as well as the decidability of membership in equational theory generated by the representation class. Although the property fails for the language of Relation Algebras, it remains an open question for many of its reduct languages. We examine the conjecture that a reduct language of Re- lation Algebra has the FRP if and only if it does not include negation and composition, nor meet and composition. Here we prove that any signature containing composition and negation fails to have the FRP. This preliminary result, together with FRP failing for any signature containing composition and meet [Neu16], proves the right to left implication of the conjecture. For the left to right implication, the FRP is known to hold for composition-free signatures as well as a handful of those containing composi- tion. Furthermore, we show here that in any reduct signature with composition but neither meet nor negation a [finite] representable structure has a [finite] representation if and only if it embeds into a [finite] Relation Algebra (not necessarily representable). This suggests that well known counterexamples to FRP in other signatures, like the Point Algebra will have a finite base representation in signatures conjectured to have the FRP. Finally, we look at signatures, like that of join-lattice semigroups, where embedding a finite representable structure into a finite relation algebra appears to be especially difficult and look at examples of some of the more interesting known such embeddings.
    </div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T15:40:00">16:40</a></td>
    <td align="left"><i ><u >Roland Glück</u></i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T41')">On the Computation of Isolated Sublattices (short talk)</a>
    <div style="display:none", id="T41"><br /><br />In this short notice we give somei deas how toc ompute isolated sublattices which can be used to derive a recursive algorithm for the com- putation of the number of closure operators on a finite lattice. We give an asymptoticaly optimal algorithm for deciding the existence and - in the case of existence - the computation of useful nontrivial isolated summit sublattices. The general case (i.e., an optimal algorithm for the computa- tion of general nontrivial useful isolated sublattices) remains unsolved, however, we try to give some ideas and hints for future research.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T16:00:00">17:00</a></td>
    <td align="left"><i >Manfred Droste, <u >Sven Dziadek</u>, and Werner Kuich</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T42')">Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages (short talk)</a>
    <div style="display:none", id="T42"><br /><br />In weighted automata theory, many classical results on formal languages have been ex- tended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of (mixed) ω-algebraic systems of equations and by weighted ω-pushdown automata.
    In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ε-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.</div>
    </td>
    </tr>
    
    
    
    
    <tr style="background-color:#fafcff", valign="top">
    <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T16:20:00">17:20</a></td>
    <td align="left"><i ><u >Uli Fahrenberg</u>, Christian Johansen, Georg Struth, Krzysztof Ziemiański</i></td>
    <td align="left", width="60%">
    <a href="javascript:toggleDiv('T43')">Languages of Higher-Dimensional Automata (short talk)</a>
    <div style="display:none", id="T43"><br /><br />We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties.  To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency.  HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells.  Their languages are sets of interval orders closed under subsumption; as a major technical step we expose a bijection between interval orders and a subclass of HDAs.  We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.
    
    This work is part of an ongoing program to develop a theory of regular concurrent languages.  In RAMiCS-18 the first three authors together with Ratan Bahadur Thapa introduced gluing-parallel posets with interfaces as a model for concurrent Kleene algebra.  Here we develop the basics of HDA languages as sets of gluing-parallel pomsets, and in currently ongoing work we prove a Kleene theorem for such languages.
    
    This talk is based on arxiv:2103.07557 which has recently been accepted for publication in MSCS.  In the talk I will put this work in the context above.</div>
    </td>
    </tr>
    
    
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-05T18:30:00">19:30</a></td><td colspan="2", style="padding:5pt"><b >Dinner</b></td></tr>
    <tr ><th colspan="3", style="padding:10pt">Saturday November 6, 2021</th></tr>
    <tr valign="top"><td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-06T06:00:00">7:00</a></td><td colspan="2", style="padding:5pt"><b >Breakfast</b></td></tr>
    </table>
    
    
          <!-- End program -->
    
          
    <!--      <h3 id="dinner">Workshop Dinner</h3> -->
    
          <h3 id="cfp">Call for papers</h3>
    
          <p>Submission is via EasyChair
    	at <a href="https://www.easychair.org/conferences/?conf=ramics2021">https://www.easychair.org/conferences/?conf=ramics2021</a>.</p>
    
          <a href="https://link.springer.com/conference/ramics"><img src="LNCS-Logo.jpg"
          width="30%" alt="Springer LNCS logo" title="Springer LNCS logo"
          style="float:right; margin-top:0px; margin-bottom:0px;
          margin-left:20px; margin-right:0px" /></a>
          
          <p>All papers will be peer-reviewed by at least three
    	referees. The proceedings will be published in an LNCS volume
    	by Springer, ready at the conference. Submissions must not be
    	published or under review for publication
    	elsewhere. Submissions must be in English using a PDF not
    	exceeding <em>16 pages</em> in LNCS style.</p>
    
          <p>Submissions must provide sufficient information to judge
    	their merits. Additional material may be provided in a clearly
    	marked appendix or by a reference to a manuscript on a web
    	site. Experimental data, software or mathematical components
    	for theorem provers must be available in sufficient detail for
    	referees. Deviation from these requirements may lead to
    	rejection.</p>
    
          <p>One author of each accepted paper is expected to present the
    	paper at the conference. Accepted papers must be produced with
    	LaTeX. Formatting instructions and LNCS style files are
    	available
    	at <a href="http://www.springer.de/comp/lncs/authors.html">http://www.springer.de/comp/lncs/authors.html</a>.</p>
    
          <p>As for earlier RAMiCS conferences, we intend to publish a
    	journal special issue with revised and extended versions of a
    	selection of the best papers.</p>
    
          <h3 id="cfsc">Call for short contributions/posters</h3>
    
          <p>Additionally to the standard CfP, RAMiCS is also calling for
    short contributions and posters.  We are hence calling for
    presentations of original, unfinished, already published, or otherwise
    interesting work within the topics of the RAMiCS conferences.  The
    submission can be in the form of a poster, an abstract, a paper
    submitted to or published at another conference, etc.  Short
    contributions will <bf>not</bf> be published in the conference
    proceedings.</p>
    
          <p>Please send your short submission
    	to <a href="mailto:ramics2021@easychair.org">ramics2021@easychair.org</a>
    	by 29 August 2021.</p>
          
          <!--
          <p>As a novelty this year, and additionally to the standard CfP,
    	RAMiCS is also calling for short contributions and posters.
    	We are hence calling for presentations of original,
    	unfinished, already published, or otherwise interesting work
    	within the topics of the RAMiCS conferences.  The submission
    	can be in the form of a poster, an abstract, a paper submitted
    	to or published at another conference, etc.  Short
    	contributions will <em>not</em> be published in the conference
    	proceedings.</p>
    
          <p>Please send your short submission
    	to <a href="mailto:ramics18-info@lists.gforge.inria.fr">ramics18-info@lists.gforge.inria.fr</a>
    	by 14 February 2021.</p>
    
          -->
          
          <h3 id="dates">Important dates</h3>
    
          <p>All dates are AoE (anywhere on Earth):
    	<ul>
    	  <li>Abstract Submission: <del>28 May 2021</del></li>
    	  <li>Paper Submission: <del>4 June 2021</del></li>
    	  <li>Author Notification: <del>23 July 2021</del></li>
    	  <li>Final Version: <del>30 July 2021</del> <del><b>19 August 2021</b></del></li>
    	  <li>Submission of Short Contributions: <del><b>29 August 2021</b></del></li>
    	  <li>Author Notification: <b><del>5 September 2021</del></b></li>
    	  <li>Registration deadline:<del>12 September 2021</del></li>
    	  <li>RAMiCS 2021: 2 to 5 November 2021</li>
          </ul></p>
    
    
          <p>Application for grants, covering lodging and catering:
    	<ul>
    	  <li>Opening: 1 July 2021</li>
    	  <li>Deadline:  12 September 2021</li>
    	  <li>Notification: before 17 September 2021</li>
          </ul></p>
    
          <h3 id="sponsors">RAMICS 2021 Sponsors</h3>
    
          <center>
    	
    	<!--
    	<a href="https://www.smf.ematd.fr/">
    	  <img src="img/logoSMF.jpeg" title="SMF" alt="SMF logo"
    	       style="margin-left:50px; margin-right:20px; max-widtd: 20%;
    		      max-height: 20%;" />
    	</a>
    	-->
    
    	<a href="https://www.lis-lab.fr/">
    	  <img src="img/logoLIS.png" title="LIS" alt="LIS logo"
    	       style="margin-left:20px; margin-right:20px; max-width: 20%;
    		      max-height: 20%;" />
    	</a>
    	
    	<a href="https://www.cirm-math.com/">
    	  <img src="img/logoCIRM.png" title="CIRM" alt="CIRM logo"
    	       style="margin-left:20px; margin-right:20px; margin-bottom:30px; max-width: 55%;
    		      max-height: 20%;" />
    	</a>
    
          </center>
    
          <p></p>
          
          <center>
    
    	<a href="https://labex-archimede.univ-amu.fr/">
    	  <img src="img/logoArchimede.png" title="Institut Archimède" alt="Archimède logo"
    	       style="margin-left:20px; margin-right:50px; max-width: 35%;
    		      max-height: 20%;" />
    	</a>
    
    	<a href="https://www.univ-amu.fr/">
    	  <img src="img/logoAMU.jpg" title="Aix-Marseille Université" alt="AMU logo"
    	       style="margin-left:50px; margin-right:20px;
    	       margin-bottom:0px; max-width: 40%;
    		      max-height: 20%;" />
    	</a>
    	
          </center>
    
          	<!--
    	<table>
    	  <tr>
    	    <td style="text-align:right;">
    	      
    	      <a href="https://www.lis-lab.fr/">
    		<img src="img/logoLIS.png" title="LIS" alt="LIS logo"
    		     style="margin-left:20px; margin-right:20px; max-width: 20%;
    			    max-height: 20%;" />
    	      </a>
    	    </td>
    	    
    	    <td style="text-align:left;">
    	      <a href="https://www.smf.ematd.fr/">
    		<img src="img/logoSMF.jpeg" title="SMF" alt="SMF logo"
    		     style="margin-left:20px; margin-right:20px; max-widtd: 20%;
    			    max-height: 20%;" />
    	      </a>
    	      
    	    </td>
    	  </tr>
    	  
    	  <tr>
    
    	    <td style="text-align:right;">
    	      <a href="https://labex-archimede.univ-amu.fr/">
    		<img src="img/logoArchimede.png" title="Institut Archimède" alt="Archimède logo"
    		     style="margin-left:20px; margin-right:20px; max-width: 40%;
    			    max-height: 20%;" />
    	      </a>
    	    </td>
    	    
    	    <td style="text-align:left;">
    	      <a href="https://www.univ-amu.fr/">
    		<img src="img/logoAMU.jpg" title="Aix-Marseille Université" alt="AMU logo"
    		     style="margin-left:20px; margin-right:20px; max-widtd: 40%;
    			    max-height: 20%;" />
    	      </a>
    
    	    </td>
    	  </tr>
    	  
    	</table>
          	-->
    
          <h3 id="contact">Contact</h3>
    
          <p><a href="mailto:ramics2021@easychair.org">ramics2021@easychair.org</a></p>
    
        </div>
        
        <!-- ###### Footer ###### -->
    
        <div id="footer">
          <div>
            Website design based on <a href="http://www.oswd.org/design/preview/id/1152">Blue Haze</a> by <a href="http://www.oswd.org/user/profile/id/3013">haran</a> from <a href="http://www.oswd.org/">OSWD</a>.  <a href="mailto:ulrich.fahrenberg@polytechnique.edu">Contact</a>
          </div>
        </div>
    
      </body>
    
    </html>