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.
