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:
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.
Here is the list of past seminars in reverse chronological order.
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.
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.