In addition to its yearly programme of taught courses on the
mathematical foundations of
computing, the Midlands Graduate School holds an afternoon of Christmas Seminars.
The seminars are free, open to everyone, and no registration is required.
14.00 - 15.00:
Coalgebra Learning via Duality
Jurriaan Rot, Radboud University Nijmegen
15.00 - 15.30:
Coffee (in the Atrium of the Computer Science building)
15.30 - 16.30:
How to Replace Sharing with Fortune-Telling
Jennifer Hackett, University of Nottingham
Lazy evaluation gives us two main benefits: compositional programming and infinite data. However, these benefits come at a cost, and one of the main reasons given in favour of strict (non-lazy) functional languages is that their operational behaviour is easier to understand. The key issue with understanding lazy evaluation is that while the external interface provided to the programmer is declarative and pure, the internal implementation is stateful. As a result, modelling lazy evaluation requires us to thread state through everything we do, vastly complicating our reasoning. In this talk, I will show how to avoid this problem by replacing the internal state of lazy evaluation with an external nondeterminism. This allows us to construct a much simplified semantics for lazy evaluation that still faithfully models concerns like efficiency.
16.30 - 17.30:
Strictly associative and unital higher category theory
Jamie Vicary, University of Birmingham
I present a new model of higher category theory which is strictly associative and strictly unital, allowing short proofs that are unencumbered by the bureaucracy of coherence. The theory is elementary, allowing it to be explained in a straightforward way, without the need for high-powered categorical technology. It is amenable to computer implementation, and we give a demonstration of a new proof assistant "homotopy.io", currently under development, which allows the user to construct proofs in a free n-category, in principle for any finite n, and visualize them geometrically as 2d and 3d diagrams. It is conjectured that, despite its strictness properties, every weak infinity-category will be equivalent to one of this new type, making this new language a fully general approach to compositional higher category theory.
(Joint work with Christoph Dorn, Christopher Douglas, and David Reutter.)
Afterwards we will go for an early dinner at Jimmy Spices, located off Broad Street.
Lecture Room UG09
Murray Learning Centre (opposite Computer Science)
University of Birmingham
A campus map and general directions are available here.
By train or bus: The "University" train station is 50 metres away from Computer Science and the Murray Learning Centre. There are direct trains from several locations but otherwise you will need to change to a local train (towards Longbridge or Redditch) at Birmingham New Street.
By car: Aim for the "North East multi storey car park". Access is via Pritchatts Road and the sat nav postcode is B15 2SA. You will need coins or the ParkMobile app.