Midlands Graduate School
in the Foundations of Computing Science 2021

In Cyberspace, 12-16 April 2021

[overview]

[programme]

News

16.04. The MGS zoom session will be closed this afternoon. The videos will remain available for all participants for the next two weeks.
08.04. Page has been updated (zoom set-up, participants talks, conference dinner, video recordings).
02.04. Registration is now closed, participants have been notified.

Overview

The annual Midlands Graduate School in the Foundations of Computing Science (MGS) offers an intensive programme of lectures on the mathematical foundations of computing. It addresses first of all PhD students in their first or second year, but is open to anyone interested in its topics, from academia to industry and around the world. The school has been run since 1999 and is hosted alternately by the Universities of Birmingham, Leicester, Nottingham and Sheffield. MGS 21 is its 21st incarnation. Information about previous events can be found at the MGS web site.

MGS 21 is virtual. It is organised by the Department of Computer Science at the University of Sheffield and hosted via Zoom by the School of Computer Science at the University of Birmingham. It starts on April 12 in the morning and finishes on April 16 in the afternoon.

Programme

MGS 21 consists of eight courses, each with four or five hours of lectures and a similar number of exercise sessions. Three of the courses are introductory and one is given by an invited lecturer. The invited lectures should be attended by all participants. The remaining courses are more advanced or specialised; participants may select them depending on their interests. All lectures are livestreamed, if possible. Video recordings are made available to participants via a link sent by email.

We are also organising an evening session where participants can briefly present their own research. More information can be found below.

To access the lecture material for individual courses, click at the titles of lectures.

Invited Lectures

The invited speaker at MGS 21 is Prof Tarmo Uustalu, Reykjavik. His lectures will be on Monads and Interaction (MAI).

Introductory Courses

Category Theory (CAT)	Jacopo Emmenegger, Birmingham
Type Theory (TYP)	Thorsten Altenkirch, Nottingham
Proof Theory (PRF)	Anupam Das, Birmingham

Advanced Courses

Homotopy Type Theory (HoTT)	Nicolai Kraus, Nottingham
Inductive and Coinductive Reasoning with Isabelle/HOL (ISA)	Andrei Popescu, Sheffield
Effects and Call-by-Push-Value (CBPV)	Paul Blain Levy, Birmingham
Formal Modelling and Analysis of Concurrent Systems (CON)	Mohammad Mousavi, Leicester

Participants' Talks

We are organising a session on Tuesday, April 13, 20:00-21:30, where MGS participants can present their own research. Titles and abstracts can be found here.

Conference Dinner

The MGS virtual conference dinner will take place on Wednesday, April 14, 20:00-21:30, in many different Zoom breakout rooms (to be set up). We will allocate participants randomly and swap between rooms every 10 minutes. Feel free to bring your own food and drinks.

[back to top]

Registration

Registration now closed.

[back to top]

Course Schedule

MGS 21 starts at 9:00 BST on Monday 12.04. and ends on Friday 16.04. in the afternoon. Although the event is virtual, lecturers, participants and organisers will come together for a week of intense learning and teaching with close personal interactions. All lectures and exercise sessions are livestreamed via Zoom, with some exceptions.

Course Time Table

coffee break (in Coffee Area and discussion rooms)

coffee break (in Coffee Area and discussion rooms)

coffee break (in Coffee Area and discussion rooms)

discussions (in Coffee Area and discussion rooms)

18:00-20:00

20:00-21:30

participants'
talks
(see schedule)

virtual
conference
dinner

The letters M, A, B, C indicate the Zoom rooms where lectures and exercise sessions take place. M is the main room, A, B, C are breakout rooms. See below for more information about the Zoom set up.

Participants' Talks Schedule

Participant's talks take place in the evening of April 13. Abstracts can be found here.

Track I (Room M)

20:00-20:15: The untyped computational lambda-calculus and its intersection type discipline
Riccardo Treglia (Universita degli Studi di Torino)

20:15-20:30: Partial Type Annotations
Pedro Ângelo ( Universidade do Porto)

20:30-20:45: A mechanical formalization of Hidnley-Damas-Milner type inference (Ongoing work)
Roger Bosman (KU Leuven)

20:45-21:00: On Structuring Pure Functional Programs Using Monoidal Profunctors
Alexandre Garcia de Oliveira (University of Sao Paulo)

21:00-21:15: Boxes and Locks
Nachiappan Valliappan (Chalmers University of Technology)

21:15-21:30: Equating polymorphic programs with the same potential utility
Cristian F. Sottile (Universidad de Buenos Aires)

Track II (Room A)

20:00-20:15: Linear logic with fixpoints from a denotational semantic point of view
Farzad Jafarrahmani (IRIF, Paris)

20:15-20:30: Paraconsistent probabilistic logics and their proof theory
Daniil Kozhemiachenko (INSA CVL, LIFO Université Orléans)

20:30-20:45: From Lindenbaum-Tarski Algebras to Classifying Toposes
Joshua Liam Wrigley (University of Insubria)

20:45-21:00: From computation to a reconstruction of (linear) logic
Boris Eng (LIPN Université Sorbonne Paris Nord, France)

21:00-21:15: Some axioms of Set Theory through the Löwenheim-Skolem Theorem
José Javier González López (University of Salamanca)

20:15-21:30: Subunits and local states
Nuiok Dicaire (University of Edinburgh)

Track III (Room B)

20:00-20:15: Measure inference and inductive lemma discovery for program termination
Rodrigo Raya (EPFL)

20:15-20:30: Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
Todd Schmid (University College London)

20:30-20:45: A Neural Compiler
Joey Velez-Ginorio (MIT, USA)

20:45-21:00: Normative Reasoning in Isabelle/HOL
Ali Farjami (University of Luxembourg)

21:00-21:15: The interplay of data and channel imperfections in verifying termination of declarative distributed systems
Francesco Di Cosmo (Free University of Bozen-Bolzano)

21:15-21:30: Asynchronous games on Petri nets
Federica Adobbati (University of Milano-Bicocca)

[back to top]

Zoom Set Up

The entire event is hosted via Zoom by the University of Birmingham. Please contact Achim Jung for all Zoom-related issues. Participants can access the main Zoom session (room M) as explained by email.

Most lectures take place within room M. Some others and all exercise sessions are scheduled within breakout rooms A, B and C as shown in the time table There is also a Coffee Area where people can meet freely and socialise. The main room and all breakout rooms will remain open throughout the event.

For the coffee breaks and beyond, participants can use the Coffee Area. There is also an additional breakout discussion room for each course where participants can meet to talk about specific topics.

[back to top]