Midlands Graduate School in the Foundations of Computing Science
Christmas Seminars
Friday 19.12.2014,
14.00-18.00
Pam Liversidge Building, PLB-LT01
The University of Sheffield
Programme
14:00-15:00
Positivity Problems for Linear Recurrence Sequences
James Worrell (Oxford)
The Positivity Problem asks whether all terms of a given linear recurrence sequence are positive. Linear recurrence sequences are ubiquitous and this decision problem arises in many settings, including formal languages, population dynamics, probabilistic model checking, loop termination, and combinatorics. It is also closely related to the Skolem-Mahler-Lech Theorem in number theory, which describes the set of zeros of a linear recurrence sequence. The Positivity Problem has been studied since the 1970s; however its decidability remains open. In this talk I will discuss the history and significance of this and related problems, some recent positive decidability results, and obstacles to further progress.
15:00-15:45 Refreshments
15:45-16:30
Curry-Howard for GUIs:
From Model-View-Controller to Classical Linear Logic
Neelakantan Krishnaswami (Birmingham)
In this talk, I will explain how realizability is better than Santa Claus. Father Christmas brings gifts of toys to good children, but realizability brings the gift of type structure to all programming languages --- regardless of whether they are good or bad! Now, modern graphical user interface are structured with an event-driven architecture. Programmers structure their programs as a collection of small imperative callbacks, which are invoked by an event loop as program events occur. That is, they must write higher-order imperative programs in continuation-passing style. This is very bad indeed! Using ideas from realizability theory (in particular, biorthogonality), it is possible to build a model of classical linear logic on top of an event-based architecture. Since classical linear logic has a proof theory in terms of process calculi, we gain a neat explanation of why programmers talk about GUI programs in terms of concurrency, even though they implement them in terms of state and control. Furthermore, we now also have a type structure upon which we can build powerful abstractions -- historically the bane of UI toolkits!
16:30-17:15
HoTT Christmas
Thorsten Altenkirch (Nottingham)
Homotopy Type Theory is a new foundation of Mathematics and a verification and programming language. I'd like to explain what is the difference of HoTT as compared to conventional foundations (Set Theory) and also what are the challenges. In particular how to run HoTT programs - here there is some recent progress in joint work with Ambrus Kaposi.
17:15-18:00
How (Not) to Define Categories in Homotopy Type Theory
James Cranch (Sheffield)
Homotopy type theory, as pioneered by Voevodsky and others, is a foundational system which promises to give convenient representations of many mathematical objects. But does it represent category theory particularly pleasantly? Assuming no understanding of homotopy type theory, I'll mention the problems involved, and describe some partial progress.
from 18:00 Pub and Restaurant
Organisation
The 2015 Christmas Seminars are hosted by the Department of Computer Science at the University of Sheffield.Please contact Georg Struth for all enquiries.
Travel
The seminars will take place at
Lecture Theatre PBL-LT01Warning: The Pam Liversage Building is essentially an annex to the Mappin Building and it is poorly signposed (we will put up special signposts for the Christmas Seminar). To find the lecture theatre, enter the Mappin Building by its main entrance. Turn left and follow the winding corridors until you reach the modern annex. Find the stairs or elevators and descend to the ground floor. The lecture hall is indicated from there.
Pam Liversidge Building
Mappin Street
Sheffield S1
United Kingdom
Please use the following links to find
- information for visitors, including maps and travel advice;
- a campus map (Mappin Building has number 170).
