Online Worldwide Seminar on
Logic and Semantics (OWLS)


The seminar has shifted later by 1 hour, and now starts at 2pm UTC
...
Introduction
The Online Worldwide Seminar on Logic and Semantics is a new series of research talks, highlighting the most exciting recent work in the international computer science logic community. The scope of the seminar series is roughly that of the major computer science logic conferences such as LICS, ICALP and FSCD. It takes place on most Wednesdays, with a focus every other week on the work of young researchers.
In this time of restricted international travel, a key aim of this series is to provide a forum for the informal discussion and social interaction that is so important for the progress of science. To facilitate this, the seminar incorporates in virtual form a number of features more normally associated with physical meetings:
 Virtual "coffee breaks" before and after the seminar, allowing participants to chat in small groups, replicating the social element of a realworld conference.
 Robust technology platform supporting hundreds of interactive participants.
 Livestream of the speaker's slides visible alongside the speaker's face, allowing nuanced communication at a human level.
 Chairperson to introduce the speaker, facilitate questions from the audience, and keep proceedings running on time.
 Audience members whose question is selected by the chairperson can deliver it in full audio and video, giving a natural interaction with the speaker.
 No need to register, just show up.
Talks are given by invitation of the organizing committee. Feedback is warmly encouraged; if you have any comments or ideas, feel free to get in touch with an organizer.
Mailing list
The OWLS mailing list sends reminders before each seminar, and announces upcoming seminars. To subscribe, or manage an existing subscription, visit this link:
Messages will be sent from the address clowls@lists.cam.ac.uk.
Programme
Time change: seminars now take place on Wednesdays at 3pm in the UK, which is 2pm UTC. An easy way to see the corresponding time in your own time zone is to add the OWLS calendar to your own calendar, with the following links: Google Calendar Apple Calendar
Seminars are 45 minutes long including questions, and will start at the advertised time. As described below, feel free to join early, or stay around after the end of the talk, to participate in the coffee breaks. A link to join the seminar is given in the participant information below. Every other week, the seminar hosts a young researcher to present their work; these seminars are labelled OWLSYR.
Here is the list of upcoming seminars.
 21 October 2020 (OWLS). Antonin Kucera, Masaryk University, "Efficient analysis of VASS termination complexity". Chair: Pawel Sobocinski
 28 October 2020 (YROWLS). Sebastian Junges, UC Berkeley, "Finding Memoryless Policies in Partially Observable MDPs is 'Existential Theory of the Reals'complete". Chair: Nathanaël Fijalkow
 4 November 2020 (OWLS). Orna Kupferman, Hebrew University, TBA. Chair: Alexandra Silva
 18 November 2020 (OWLS). Joël Ouaknine, Max Planck Institute for Software Systems, "Holonomic Techniques, Periods, and Decision Problems". Chair: Pawel Sobocinski
Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I will give an overview of the area, and in particular will present a select survey of known and original results on decision problems for holonomic sequences and functions. I will also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I will relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.
Parts of this talk will be based on the paper "On Positivity and Minimality for SecondOrder Holonomic Sequences", https://arxiv.org/abs/2007.12282.
 25 November 2020 (YROWLS). Francesco Gavazzo, University of Bologna, "Modal Reasoning = Metric Reasoning, via Lawvere". Chair: Charles Grellois
 2 December 2020 (OWLS). Derek Dreyer, MPISWS, TBA. Chair: Alexandra Silva
 9 December 2020 (YROWLS). Maaike Zwart, University of Oxford, "Distributive Laws in the Boom Hierarchy". Chair: Koko Muroya
Here is the list of past seminars in reverse chronological order.
 14 October 2020 (YROWLS). Henning Basold, Universteit Leiden, "Coalgebraic Communication Protocols and Session Types". Chair: Koko Muroya
This is joint work with Alex Keizer and Jorge A. Pérez.
Compositional methods are central to the development and verification
of software systems. They allow to break down large systems into
smaller components, while enabling reasoning about the behaviour of the
composed system. For concurrent and communicating systems, compositional
techniques based on *behavioural type systems* have received much
attention. By abstracting communication protocols as types, these type
systems can statically check that programs interact with channels
according to a certain protocol, whether the intended messages are
exchanged in a certain order. For this talk, we will put on our
coalgebraic spectacles to investigate *session types*, a widely studied
class of behavioral type systems. We will seek a syntaxfree
description of sessionbased concurrency as states of coalgebras. The
result will be a description of type equivalence, duality, and subtyping
relations in terms of canonical coinductive presentations. In turn,
this coinductive presentation makes it possible to elegantly derive a
decidable type system with subtyping for πcalculus processes, in which
the states of a coalgebra will serve as channel protocols. Going full
circle, we will also exhibit a coalgebra structure on an existing
session type system, and show that the relations and type system
resulting from our coalgebraic perspective agree with the existing ones.
 7 October 2020 (OWLS). Andrej Bauer, University of Ljubljana, "Effects in the real world". Chair: Pawel Sobocinski (video)
Joint work with Danel Ahman, University of Ljubljana.
In modern languages, computational effects are often structured using monads or algebraic effects and handlers. These mechanisms excel at implementation of computational effects within the language itself. For instance, the familiar implementation of mutable state in terms of statepassing functions requires no native state, and can be implemented either as a monad or using handlers. One is naturally drawn to using these techniques also for dealing with actual effects, such as manipulation of native memory and access to hardware. These are represented inside the language as algebraic operations or a monad, but treated specially by the language's toplevel runtime, which invokes corresponding operating system functionality. While this approach works in practice, one wishes that the ingenuity of the language implementors were better supported by a more flexible methodology with a sound theoretical footing.
We address the issue by showing how to design a programming language based on runners of algebraic effects. We review runners, recast them as a programming construct, and present a calculus that captures the core ideas of programming with them. Through examples of runners we show how they capture both the interaction between the program and the external world, and encapsulation of programs in virtual environments that tightly control access to external resources and provide strong guarantees of proper resource finalization.
We accompanied our work with a prototype programming language Coop (https://github.com/andrejbauer/coop) and a Haskell library for runners (https://github.com/danelahman/haskellcoop).
References:
 30 September 2020 (YROWLS). Ryoma Sin'ya, Akita University, "Asymptotic Approximation by Regular Languages". Chair: Koko Muroya
(slides) (video)
In this talk we will introduce a new property of formal languages called REGmeasurability where REG is the class of regular languages.
Intuitively, a language L is REGmeasurable if there exists an infinite sequence of regular languages that ``converges'' to L.
A language without REGmeasurability has a complex shape in some sense so that it can not be approximated by regular languages.
The motivation, why we have been interested in REGmeasurability, originally came from the following conjecture posed by [DömösiHorvathIto 1991]:
the set of all primitive words over a nonsingleton alphabet is not contextfree.
We will describe that several contextfree languages are REGmeasurable (including languages with transcendental generating function and transcendental density, in particular),
while a certain simple deterministic contextfree language and the set of primitive words are REGimmeasurable in a strong sense.
We will also discuss some open problems and future work.
This talk is based on the following work: http://www.math.akitau.ac.jp/~ryoma/misc/measure.pdf
 23 September 2020 (OWLS). Anupam Das, University of Birmingham, "Cyclic proofs, Peano arithmetic, and Logical complexity". Chair: Jamie Vicary (video)
Cyclic proof theory is an increasingly popular tool for (co)inductive reasoning in algebras, type systems, modal fixed point logics and predicate logics with inductive definitions. Understanding the relative power of cyclicity and induction constitutes one of the key questions traversing these areas.
The setting of firstorder arithmetic provides us with well understood delineations of proof theoretic expressivity, namely in terms of *logical complexity*, i.e. the number of quantifier alternations required for formulas occurring in a proof. We show that cyclic proofs in arithmetic are strictly more succinct than inductive ones in this sense, refining a recent result that cyclic arithmetic and Peano arithmetic are equivalent [Simpson '17] cf. also [Berardi & Tatsuta '17]. We give a converse result too, thus classifying the proof theoretic strength of cyclic arithmetic theories with restricted logical complexity. The former result is based on structural proof theoretic techniques, namely a form of cutelimination, while the latter result requires us to adapt recent results on the reverse mathematics of omegaword automaton theory [Kołodziejczyk, Michalewski, Pradic & Skrzypczak '16] with classical proof theoretic methods.
Given the uniformity of our approach, we are able to recover a metamathematical account of our cyclic theories too. As a result we partially resolve an open problem on the logical strength of McNaughton's theorem on determinisation of omegaword automata from [Kołodziejczyk, Michalewski, Pradic & Skrzypczak '16], by reduction to a form of Gödel incompleteness for cyclic theories.
This talk is based on the following work: https://arxiv.org/abs/1807.10248.
References:

[Berardi & Tatsuta '17] Equivalence of inductive definitions and cyclic proofs under arithmetic. Proceedings of LICS 2017.

[Kołodziejczyk, Michalewski, Pradic & Skrzypczak '16] The Logical Strength of Büchi's Decidability Theorem. Proceedings of CSL '16.

[Simpson '17] Cyclic Arithmetic Is Equivalent to Peano Arithmetic. Proceedings of FoSSaCS 2017.
 9 September 2020 (OWLS). Filippo Bonchi, Universita di Pisa, "Functorial Semantics: from Lawvere to CarboniWalters". Chair: Pawel Sobocinski (video)
Various kinds of relational algebras have been studied since long time. The traditional approach consists in giving an algebraic theory, namely a signature and a set of equations. Unfortunately, the equations often turn out to be incomplete, unless one uses more sophisticated logics (e.g, Horn clauses).
In this talk, we advocate the use of a different sort of algebra, where terms are not anymore trees but rather graphs. This has a clear categorical justification that can be clearly expressed by mean of functorial semantics by Lawvere. We start by gently introducing the Lawvere's approach and then explain its relational extension to Cartesian Bicategories by Carboni and Walters.
 2 September 2020 (OWLS DEBATE), 3pm UTC. Panel: Brendan Fong, MIT; Nicole Immorlica, Microsoft Research; Delia Kesner, Université de Paris (IRIF); Benjamin Pierce, University of Pennsylvania; Thomas Schwentick, Technische Universität Dortmund; Moshe Vardi, Rice University. "Evolution or Revolution? The Future of Conferences in Theoretical Computer Science". Chair: Jamie Vicary (video)
The entire community is invited to participate in a debate on the future of the conference system in theoretical computer science. This will provide a rare communitywide opportunity for us to discuss the strengths and weaknesses of our current system, and consider if we can do better. Questions will be asked by members of the audience, and answered by our panel members.
The scope of the debate is all aspects of our publishing and community
traditions, characterised by prestige earned mostly through
publication in competitive conferences, and frequent local and
international travel. Possible topics for discussion include the need
to publish in conferences for career progression, which usually
involves burning carbon; wasted reviewing effort when good papers are
rejected from highly competitive conferences; the extent of our
responsibility as a community to respond to climate change;
alternative publishing models, like the journalfocussed system used
in mathematics; high costs of conference travel and registration;
virtual conference advantages, disadvantages and best practice;
improving equality, diversity and access; consequences and response to
COVID19; and the role of professional bodies. These topics have many
tight relationships, and need to be discussed together to gain a full
understanding of the issues involved.
Poll responses. Here are the results of the three anonymous polls that were held during the debate.

Until recently, it was common for members of the TCS community to make regular flights. If COVID19 can be resolved soon with a widelyavailable vaccine, should we try as a community to:
 go back to our usual flight habits (i.e. flying several times per year) (2 responses, 3%)
 continue regular flights, but at a substantially reduced frequency (i.e. flying a couple of times per year) (58 responses, 73%)
 almost completely eliminate flights (i.e. flying a few times per career) (19 responses, 24%)

Most researchers in TCS follow the "conference first" model, in which results are published first in a conference (either physical or virtual, and preferably highstatus), and later on in a journal in expanded form. As a community, should we aim to:
 continue this into the future (43 responses, 32%)
 switch to a "journal first" model more like mathematics, changing the TCS conference system so presentation of a paper does not imply publication in an associated proceedings volume (91 responses, 68%)

For the purposes of professional networking and scholarly communication in TCS, virtual conferences can be:
 just as effective as physical conferences, or even more effective (28 responses, 20%)
 less effective than physical conferences, but still reasonably effective (67 responses, 47%)
 much less effective than physical conferences (48 responses, 34%)
The following links provide further reading on topics related to the debate:
 26 August 2020 (OWLS). Orna Grumberg, Technion  Israel Institute of Technology , "Automated Program Repair". Chair: Alexandra Silva (video) In the process of software development and maintenance, much efforts are invested in order to
ensure that the product is as bug free as possible. Automating the repair process is highly
desired.
In this talk we present two approaches to automated program repair, based on formal methods.
The first approach automatically repairs an erroneous program
using a predefined set of mutations to the code (e.g., replacing ‘+’ with ‘‘ ; ‘>’ with ‘<’, etc.).
The repair algorithm goes through generatevalidate iterations, which involve fault localization
mechanism in order to disregard sets of unsuccessful repairs.
The approach guarantees soundness and completeness with respect to a bounded notion of
correctness.
The second approach intertwines compositional AssumeGuarantee verification with repair.
Automata learning is used for compositional verification. If an erroneous behavior is found,
abduction assists in repairing the system by inferring new constraints that eliminate erroneous
runs. Then, the verification proceeds for the repaired system.
This is a joint work with: Hadar Frenkel, Corina Pasareanu, Batchen Rothenberg and Sarai
Sheinvald.
 12 August 2020 (OWLS). Javier Esparza, Technical University of Munich, "An Efficient Normalisation Procedure for Linear Temporal Logic". Chair: Pawel Sobocinski (video)
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a normal form for
formulas of LTL with past operators, which Manna and Pnueli then used as the
basis of their famous classification of temporal formulas. Some years later,
Chang, Manna, and Pnueli built on this result to derive a similar normal form for
the future fragment of LTL. Both normalisation procedures had a nonelementary
worstcase blowup, and followed an involved path from LTL formulas to counterfree
automata to starfree regular expressions and back to LTL.
We improve on both points. We present a purely syntactic normalisation procedure
from LTL to LTL, with single exponential blowup, that can be implemented in a few
dozen lines of Standard ML code. As an application, we derive a simple algorithm to
translate LTL into deterministic Rabin automata. The algorithm normalises the
formula, translates it into a special very weak alternating automaton, and applies a
simple determinisation procedure, valid only for these special automata.
This is joint work with Salomon Sickert that appeared in LICS 2020
 5 August 2020 (OWLSYR). Umang Mathur, University of Illinois at Urbana Champaign, "Verification of Uninterpreted and Partially Interpreted Programs". Chair: Krishna. S
(slides) (video)
Uninterpreted programs are sequential programs with loops and recursion written over a first order vocabulary where the constant, function and predicate symbols used are completely uninterpreted. The input to an uninterpreted program is a first order structure which also determines the semantics of such a programs. The verification question in this setting asks if an uninterpreted a program meets all its assertions on all input structures. In this talk, I will discuss the decidability boundaries for the verification question of uninterpreted programs. In general, the problem is undecidable, but becomes decidable for a subclass, called coherent uninterpreted programs. The decidability result is tight in that slightly relaxing the coherence criteria leads to undecidability.
I will then discuss how the decidability result of coherent programs segue into more general classes of programs, called kcoherent programs (k is a natural number). Finally, I will discuss extensions to the verification question for partially interpreted programs, where the vocabulary is associated with an underlying first order theory and the inputs are those first order structures which are also models of this underlying theory.
 29 July 2020 (OWLS). Tarmo Uustalu, Reykjavik University, "Interaction laws of monads and comonads". Chair: Jamie Vicary (slides) (video) We introduce and study functorfunctor and monadcomonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effectperforming machines. Monadcomonad interaction laws are monoid objects of the monoidal category of functorfunctor interaction laws. We show that, for suitable generalizations of the concepts of dual and Sweedler dual, the greatest functor resp. monad interacting with a given functor or comonad is its dual while the greatest comonad interacting with a given monad is its Sweedler dual. We relate monadcomonad interaction laws to stateful runners. We show that functorfunctor interaction laws are Chu spaces over the category of endofunctors taken with the Day convolution monoidal structure. Hasegawa's glueing endows the category of these Chu spaces with a monoidal structure whose monoid objects are monadcomonad interaction laws.
This is joint work with Shinya Katsumata (NII, Tokyo) and Exequiel Rivas (Inria, Paris).
 22 July 2020 (OWLSYR). Justin Hsu, University of Wisconsin–Madison, "A separation logic for probabilistic independence". Chair: Koko Muroya
(slides) (video)
Probabilistic independence is a useful concept for describing the result of random samplinga basic operation in all probabilistic languagesand for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We propose a probabilistic separation logic PSL, where separation models probabilistic independence, based on a new, probabilistic model of the logic of bunched implications (BI). The program logic PSL is capable of verifying informationtheoretic security of cryptographic constructions for several wellknown tasks, including private information retrieval, oblivious transfer, secure multiparty addition, and simple oblivious RAM, while reasoning purely in terms of independence and uniformity. If time permits, we will also discuss ongoing work for reasoning about conditional independence.
 15 July 2020 (OWLS). Christine Tasson, IRIF, Paris, "Towards a model of mixed linear and nonlinear substitution." Chair: Alexandra Silva (video)
A functional program is said to be linear when it uses exactly once its
input. Linearity is useful to handle memory safely, singleuse channels
in concurrency, or quantum resources. Yet, we do not want all inputs to
be linear and some of them can be used several times safely. Hence the
need to understand what is a model of linearnonlinear substitution.
Such settings appear naturally in differential lambdacalculus which is
our initial motivation.
We move from the usual categorical axiomatization of linear logic and
lambdacalculus to the multicategorical axiomatisation, using
profunctors and 2 monads to give account to linear and nonlinear
contexts. We present how to combine the linear and the nonlinear 2
monads in order to model the linearnonlinear substitution.
This is joint work with Martin Hyland.
 1 July 2020 (OWLSYR). Amina Doumane, CNRS, ENS de Lyon, "(Non)axiomatizability of positive relation algebras via graph homomorphisms". Chair: Charles Grellois (video)
We study the equational theories of composition and intersection on binary relations, with or without their associated neutral elements (identity and full relation). Without these constants, the equational theory coincides with that of semilatticeordered semigroups. We show that the equational theory is no longer finitely based when adding one or the other constant—contradicting a conjecture from the litterature. Our proofs exploit a characterisation in terms of graphs and graph homomorphisms, which we show how to adapt in order to capture standard equational theories over the considered signatures.
 24 June 2020 (OWLS). Valeria Vignudelli, ENS Lyon, "Monads and Quantitative Equational Theories for Nondeterminism and Probability". Chair: Pawel Sobocinski (video) The monad of convex sets of probability distributions is a wellknown tool for modelling the combination of nondeterministic and probabilistic computational effects. In this talk I will discuss theories allowing us to reason equationally about this monad, and applications to program verification.
In order to reason about distances between programs combining nondeterminism and probabilities, the monad of convex sets of distributions can be lifted from the category of sets to the category of metric spaces. Using the framework of quantitative algebras, recently introduced by Mardare, Panangaden, and Plotkin, we derive an equational presentation of this monad on metric spaces.
The main results I will present in this talk are based on collaborations with Filippo Bonchi, Matteo Mio, and Ana Sokolova.
 17 June 2020 (OWLSYR). Marie Fortin, University of Liverpool, "FO = FO3 for Linear Orders with Monotone Binary Relations" Chair: Nathanaël Fijalkow
(slides)
It is wellknown that linear orders have the 3variable property, meaning that over linear orders, every monadic firstorder formula with up to 3 free variables is equivalent to one that uses at most 3 variables in total. Over the years, this has been extended to richer classes of structures, such as realtime signals with the +1 relation, Mazurkiewicz traces, or message sequence charts. In this talk, I will present a unifying proof that generalizes those facts. It is based on starfree PDL, a variant of propositional dynamic logic that captures precisely the 3variable fragment of firstorder logic. More precisely, I will show that over structures consisting of one linear order and arbitrarily many binary relations satisfying some monotonicity conditions, starfree PDL has the same expressive power as full firstorder logic. This implies that any class of such structures has the 3variable property.
 10 June 2020 (OWLS). Seminar cancelled in support of Black Lives Matter.
 3 June 2020 (OWLSYR). Dmitry Chistikov, University of Warwick, "Parikh's theorem from the complexity viewpoint". Chair: Krishna S. (video)
(slides)
Parikh's theorem (1961) connects two basic concepts in computer science,
recursion and iteration. It states that commutative images of contextfree
and regular languages form the same family  namely semilinear sets, or
sets definable in Presburger arithmetic (the firstorder logic of addition
and order). This theorem has become a standard tool in the theory of
verification, with many different proofs and extensions.
In this talk, we will recall Parikh's theorem and look at it from the
complexity viewpoint. Transformation from pushdown automata into finite
automata incurs a description blowup, but how big does it need to be?
We will look at contextfree languages in general and at their subclass,
onecounter languages, focusing in particular on lower bounds (hardness).
 27 May 2020 (OWLS). Dexter Kozen, Cornell University, "Brzozowski derivatives as distributive laws". Chair: Alexandra Silva (slides) (video)
 13 May 2020 (OWLS). Bartek Klin, Warsaw University, "Monadic monadic second order logic". Chair: Jamie Vicary (slides) (video) Monadic second order logic (MSO) is usually studied over specific kinds of structures, be it finite words, infinite words, finite or infinite trees, total orders of various shapes, etc. A monad is a notion of "a kind of structures" that covers these and many other examples. One can formulate an abstract definition of MSO for a generic monad. I will explain how this is done, and I will describe some conditions that a monad should satisfy to ensure a basic "sanity check": that every definable language is recognized by a finite algebra. (joint work with Mikołaj Bojańczyk and Julian Salamanca)
 29 April 2020 (OWLS). Daniela Petrisan, University of Paris, "Combining probabilistic and nondeterministic choice via weak distributive laws" (video). Chair: Pawel Sobocinski
 15 April 2020 (OWLS). JoostPieter Katoen, RWTH Aachen University, "Termination of probabilistic programs". Chair: Alexandra Silva (slides) (video)
Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe randomised algorithms and more recently received attention in machine learning. Probabilistic termination has several nuances and has some unexpected effects. Programs may diverge with zero probability; they almostsurely terminate (AST). Two ASTprograms run in sequence may have an infinite expected runtime, though each of its constituents has a finite expected runtime.
This talk will demystify the notions of probabilistic termination, its surprising effects, and its hardness ("degree of undecidability"). We will show a simple proof rule for deciding AST.
 1 April 2020 (OWLS). Kevin Buzzard, Imperial College London, "Is HoTT the way to do mathematics?". Chair: Jamie Vicary (slides) (video)
Homotopy type theory (HoTT) is a foundation for mathematics. Its origins are in work of Awodey, Warren and independently Voevodsky, an algebraic geometer who then changed area and proposed a new definition of equality between mathematical objects. Voevodsky was initially motivated by a desire to formally verify his own work on a computer. However after his unfortunate death in 2017 it was still not the case that any serious algebraic geometry recognisable to a classical algebraic geometer had been formalised in a HoTT computer system. Even in 2020 Grothendieck's original definition of a scheme (the fundamental building block of modern algebraic geometry) has only been formalised in Lean's Dependent Type Theory (DTT), and not in any HoTT system.
In my talk, I will start by explaining Voevodsky's univalence axiom, the problems it solves and the problems it causes. I will then explain a basic mathematical question for which Voevodsky's axiom seems in theory like it might be helpful. I will finally talk about work of Ramon Fernandez Mir on formalising Grothendieck's original definition of a scheme in Lean's DTT system (without Voevodsky's axiom). Whether or not this can be done in a HoTT system is apparently an open problem, but one which is easily attackable, and I will finish by explaining my plan for attacking it.
Information for participants
Joining the seminar. To join any OWLS seminar, visit the following link, up to 15 minutes before the posted start time:
You will be given the option to join through your web browser, or to launch the Zoom client if it is installed on your device (see below). For the best experience, we recommend using the client. When prompted for your name, please enter your real name, so that social interactions during the seminar and coffee breaks can be more natural.
Audio and video. We encourage all participants to enable their audio and video at all times (click "Use Device Audio" in the Zoom interface.) Don't worry about making noise and disrupting the proceedings accidentally; the Chairperson will ensure your audio is muted by default during the seminar. Having your audio and video enabled will allow other participants to see your face in the "Gallery" view, letting them know that you're taking part. It also gives you the option of asking a question, and of making best use of the "coffee break" sessions. For most users with good network access (such as a fast home broadband connection), there is no need to worry that having your audio and video enabled will degrade the experience; the technology platform ensures that the speaker's audio/video stream is prioritised at all times. However, those on slow connections may find it better to disable their audio and video.
Coffee breaks. Every OWLS seminar has two "coffee breaks", one starting 15 minutes before the posted start time of the seminar, and the second starting after the seminar is finished. To participate in these, feel free to join the meeting early, or to keep the meeting window open after the end of the talk. During these coffee break periods, participants will be automatically gathered into small groups, assigned at random; please introduce yourself to the other members of your group, and chat just like you would at a real conference. Remember to bring your own coffee! If you're not interested in chatting, please close the meeting window during the coffee break periods, so that people who want to chat are not grouped with those who do not.
During the seminar. If you'd like to ask a question, either during the seminar or in the question period at the end, click the "Participants" menu and select "Raise hand". The Chairperson may choose to interrupt the speaker and give your audio/video feed the focus, giving you the opportunity to ask your question verbally, or may instead decide to let the seminar continue. You may click "Lower hand" at any time to show you no longer wish to ask a question. To preserve the experience of a real facetoface conference, there is no possibility of giving a written question, and the chat room is disabled. You also have the opportunity to give nonverbal feedback to the speaker by clicking the "speed up" or "slow down" buttons, also in the "Participants" menu.
Recordings. Most OWLS seminars will be recorded and uploaded to YouTube after the event. Only the audio/video of the chairperson, speaker, and questioners will be captured. If you prefer not to be recorded, do not ask a question. Of course, the organizers do not make any recordings of the coffee break sessions.
Inappropriate behaviour. The organizers make use of a range of security features to ensure that the seminar cannot be disrupted by participants who are not interested in constructive scientific interaction. During a seminar, if you observe ongoing inappropriate behaviour, please send a private message to the chairperson to point it out.
Technology platform
Seminars are hosted through the video conferencing system Zoom. Native clients are available to download for a wide range of platforms, including mobile devices:
For those who prefer not to use a client, a browser interface is also available.
Organizing committees
If you have any feedback about OWLS, feel free to get in touch with an organizer.
OWLS
OWLSYR
 Nathanaël Fijalkow, CNRS, Laboratoire Bordelais de Recherche en Informatique, France
 Charles Grellois, Université AixMarseille, France
 S. Krishna, IIT Bombay, India
 Koko Muroya, RIMS, Kyoto University, Japan