## Online Worldwide Seminar on## Logic and Semantics (OWLS) |

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 every Wednesday at 2pm UTC+1, 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 real-world conference.
- Robust technology platform supporting hundreds of interactive participants.
- Live-stream 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.

Here is the list of upcoming seminars. Every other week, the seminar hosts a young researcher to present their work; these seminars are labelled OWLS-YR.

Seminars take place on Wednesdays at 2pm UK time, which is currently UTC+1. 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.

- 3 June 2020 (OWLS-YR). Dmitry Chistikov, University of Warwick, "Parikh's theorem from the complexity viewpoint".
*Chair: Krishna S.*(slides) Parikh's theorem (1961) connects two basic concepts in computer science, recursion and iteration. It states that commutative images of context-free and regular languages form the same family --- namely semilinear sets, or sets definable in Presburger arithmetic (the first-order 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 context-free languages in general and at their subclass, one-counter languages, focusing in particular on lower bounds (hardness). - 10 June 2020 (OWLS). Valeria Vignudelli, ENS Lyon, "Monads and Quantitative Equational Theories for Nondeterminism and Probability".
*Chair: Pawel Sobocinski*The monad of convex sets of probability distributions is a well-known 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 (OWLS-YR). Marie Fortin, University of Liverpool, "FO = FO3 for Linear Orders with Monotone Binary Relations"
*Chair: Nathanaël Fijalkow*It is well-known that linear orders have the 3-variable property, meaning that over linear orders, every monadic first-order 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 real-time 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 star-free PDL, a variant of propositional dynamic logic that captures precisely the 3-variable fragment of first-order logic. More precisely, I will show that over structures consisting of one linear order and arbitrarily many binary relations satisfying some monotonicity conditions, star-free PDL has the same expressive power as full first-order logic. This implies that any class of such structures has the 3-variable property. - 24 June 2020 (OWLS). Anupam Das, University of Birmingham, "TBA".
*Chair: Jamie Vicary* - 1 July 2020 (OWLS-YR). Amina Doumane, CNRS, ENS de Lyon, "(Non)axiomatizability of positive relation algebras via graph homomorphisms".
*Chair: Charles Grellois* - 15 July 2020 (OWLS). Christine Tasson, IRIF, Paris, "TBA".
*Chair: Alexandra Silva* - 22 July 2020 (OWLS-YR). Justin Hsu, University of Wisconsin–Madison, "A separation logic for probabilistic independence".
*Chair: Koko Muroya*Probabilistic independence is a useful concept for describing the result of random sampling---a basic operation in all probabilistic languages---and 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 information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party 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. - 29 July 2020 (OWLS). Tarmo Uustalu, Reykjavik University, "TBA".
*Chair: TBA* - 12 August 2020 (OWLS). Javier Esparza, Technical University of Munich, "TBA".
*Chair: Alexandra Silva* - 9 September 2020 (OWLS). Filippo Bonchi, Universita di Pisa, "TBA".
*Chair: TBA*

Here is the list of past seminars in reverse chronological order.

- 27 May 2020 (OWLS). Dexter Kozen, Cornell University, "Brzozowski derivatives as distributive laws".
*Chair: Alexandra Silva* - 13 May 2020 (OWLS). Bartek Klin, Warsaw University, "Monadic monadic second order logic".
*Chair: Jamie Vicary*(slides) 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 non-deterministic choice via weak distributive laws" (video).
*Chair: Pawel Sobocinski* - 15 April 2020 (OWLS). Joost-Pieter Katoen, RWTH Aachen University, "Termination of probabilistic programs".
*Chair: Alexandra Silva*(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 almost-surely terminate (AST). Two AST-programs run in sequence may have an infinite expected run-time, though each of its constituents has a finite expected run-time.

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.

*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 face-to-face 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.

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.

The OWLS mailing list sends reminders before each seminar, and announces upcoming seminars. To sign up, visit this link:

If you have any feedback about OWLS, feel free to get in touch with an organizer.

- Alexandra Silva, University College London, UK
- Pawel Sobocinski, Tallinn University of Technology, Estonia
- Jamie Vicary, University of Cambridge, UK

- Nathanaël Fijalkow, CNRS, Laboratoire Bordelais de Recherche en Informatique, France
- Charles Grellois, Université Aix-Marseille, France.
- S. Krishna, IIT Bombay, India
- Koko Muroya, RIMS, Kyoto University, Japan