Midlands Graduate School

in the Foundations of Computing Science

Christmas Seminar 2021

Thursday, 16 December 2021, from 14:30
ONLINE
hosted by: School of Computer Science
University of Nottingham
Computer Science
Copyright of picture: https://alexwilkinson.media/

Programme

14:20-14:30, Welcome
14:30-15:30, Kevin Buzzard: How to get mathematicians to use theorem provers
Until recently, only an extremely small percentage of mathematicians had heard of computer proof assistants, and most of us only knew about them via the canonical joke that in fact they should be called computer proof obstructors. So faced with a bunch of conservative pencil-and-paper-using classical-logic-believing mathematicians, who have no understanding of equality and spend their lives flying high above the axioms, with the speaker drawing a picture and saying it's a proof, and the listeners nodding knowingly -- how do you get them to use proof assistants, when the old methods have worked for literally thousands of years? I will explain what I've been trying. Rest assured, no background in mathematics will be required.
15:30-16:00, Coffee Break
16:00-16:45, Sonia Marin: Forwarders as Process Compatibility, Logically
Session types are types for specifying protocols that processes must follow when communicating with each other. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic.
Previous work has shown that multiparty session types, generalisation of session types to protocols of three or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. Moreover, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol.
In this talk we take two steps to extend this approach. First, we generalise the concept of arbiter to that of synchronous forwarder, that is a process that implements the behaviour of an arbiter in several different ways. It provides a logical characterisation of coherence, i.e., coherence proofs can be transformed into synchronous forwarders and, viceversa, every synchronous forwarder corresponds to a coherence proofs.
Then, we generalise arbiters further to forwarders that can also display asynchronous behaviours and buffer arbitrary many messages. We show that forwarders properly extend coherence and correspond to multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs.
16:45-17:30, Artem Shinkarov: Extracting the Power of Dependent Types
Most existing programming languages provide little support to formally state and prove properties about programs. Adding such capabilities is far from trivial, as it requires significant re-engineering of the existing compilers and tools. I will present a novel technique to write correct-by-construction programs in languages without built-in verification capabilities, while maintaining the ability to use existing tools. This is achieved in three steps. Firstly, we give a shallow embedding of the language (or a subset) into a dependently typed language. Secondly, we write a program in that embedding, and we use dependent types to guarantee correctness properties of interest within the embedding. Thirdly, we extract a program written in the original language, so it can be used with existing compilers and tools.
The main insight is that it is possible to express all three steps in a single language that supports both dependent types and reflection. Essentially, this allows us to express a program, its formal properties, and a compiler for it hand-in-hand, offering a lot of flexibility to programmers. I will demonstrate the proposed technique in Agda at the example of several embedded languages.
From 17:30, Informal Chat

Venue

The continuing pandemic forces us to hold this event virtually.

Organisation

For enquiries, please contact Nicolai Kraus and Thorsten Altenkirch.