This is the Final Programme. When provided, links to pdfs of slides are now available at the end of the abstracts. Clicking on a title opens up the abstract.

All talks have taken place in room AH101, Ashdown House, Falmer Campus, University of Sussex. A campus map can be found under the "Travel" tab of this website.

Thursday 7th of September   2pm - 6pm: PhD Day

orgainsed with the help of PhD students Pancho Eliott (Sussex),  Vasilis Klimis (Sussex), and Yibei Li (Imperial College)

František Farka (Heriot-Watt): Refinement in First-Order Dependent Type Theory via Resolution

Logic programming, that is Horn Clause Logic equipped with a resolution mechanism (fohc), provides an expressive framework for first order automated theorem proving with computational advantages over alternative approaches. Traditionally, resolution mechanisms employ full unification. Recently, however, attention was given to type-theoretic interpretation of logic programming with the focus on universal fragment of fohc. In my talk, I elaborate on the idea and present a calculus in style of logic programming that accounts the full extent of fohc. The distinctive feature of the calculus is that a successful proof by resolution is captured by an explicit proof term. This calculus is a key device in a novel approach to type and term refinement in first order dependent type theory (fodtt). In my talk, I show a translation of a refinement problem in fodtt to a goal and a program in fohc and I show how to interpret an answer substitution and a proof term in fohc as a solution to the refinement problem.

Dan Saattrup Nielsen (Bristol): Jónsson Cardinals; a deceptive large cardinal notion

Does every structure have a proper elementary substructure of the same size? This question --- whose answer is false --- led to the notion of a Jónsson cardinal, being the cardinals for which this is true. These cardinals turn out to exhibit strange behaviour compared to other large cardinals, as the theory "ZFC + there is a Jónsson cardinal" is quite strong, but a Jónsson cardinal itself is ostensibly very weak in terms of direct implication. I will talk a bit about this asymmetry in strength and zoom in on the problem of determining the direct implication strength, leading to a special relationship between Jónsson cardinals and weakly compact cardinals

Peter Schrammel (Sussex & Diffblue): AI for Code

Diffblue is a recently founded Oxford-based startup. We have the ambition to automate all traditional coding tasks: bug fixing, test writing, finding and fixing exploits, refactoring code, translating from one language to another, and creating original code to fit specifications. The technology to achieve this is ready for commercialisation and we are launching our first products. We are gathering world’s leading experts in programming languages, computer-aided verification and machine learning to realise our vision to make software safer and better and cheaper to produce.

Yibei Li (Imperial): Application of logic on graphs.

Model theorists are often quite interested in homogeneous structures, which connects ideas from model theory, permutation group theory and combinatorics. The Fra{\"\i}ss{\'e} Theorem establishes a one-to-one correspondence between homogeneous structures and amalgamation classes. In this talk, I will introduce a certain class of homogeneous structures and show that the automorphism groups of the homogeneous structures corresponding to it is simple using results from model theory.

Friday 8th of September

9am Registration

Please register at the beginning of the meeting, collect lunch vouchers and other info. You should have paid beforehand. An invoice will be sent after you registered.

10am Invited Talk: Oliver Kullmann (Swansea): Big proofs and SAT 

Automated and interactive theorem proving have made strong progress over the last two decades, so that we are perhaps finally on the threshold of an age, where such systems become important tools for the working mathematician.

SAT solving, solving propositional logic, played an important role here, as the underlying logical engine. I want to report here on SAT solving for the hardest problems currently, where SAT solving has been invoked directly (see the last two entries of this Wikipedia list as examples).

Roughly speaking, the most promising approach for the hardest problems seems to be to combine "old and new", the older systematic splitting approach with the newer clause-learning approach. In this way global and local heuristics are combined, which on hard approaches can be many orders of magnitudes faster than any single approach.

SLIDES

11am Tea/Coffee

11:30am Invited Talk: Joan Bagaria (Barcelona): Strong reflection principles and the hierarchy of large cardinals

Large cardinals provide a linear measuring system for the consistency strength of theories beyond ZFC. However, the existence of large cardinals, as well as the fact that they form a linear hierarchy, are still key questions in the foundations of set theory that need further clarification. In my talk I will present some results that characterise a variety of large cardinals in terms of a uniform strong reflection principle, called Structural Reflection, which yields some insight into the existence of large cardinals as natural axioms of set theory and explains their relative strength.

SLIDES

12:30pm John Longley (Edinburgh): Robust computability notions for types arising in classical analysis 

A recurring question in computability theory has been whether one can identify a single `canonical' notion of computable operation on data of some given kind. If the data are natural numbers (or equivalently finite strings over a finite alphabet), then the existence of such a canonical notion is of course what is claimed by the classical Church-Turing thesis. If the data are themselves of a higher-order nature, then the situation is much more complex, but work of Normann (2000) and Longley (2007) has shown that even widely divergent concepts of higher-order computability will typically converge in the class of 'hereditarily total' functionals they give rise to.

I will outline some recent extensions of these results that imply the existence of similarly robust computability notions for many kinds of data arising in traditional mathematical practice, particularly complex analysis. To construct types such as the space of analytic functions on a given complex domain, one typically needs recourse not just to function spaces but also to subset and quotient types, and these constitute a non-trivial extension from the point of view of computability theory: the computable functions on a subset S of T are not immediately determined by those on T, as there may well be computable functions on S with no computable extension to T. Nevertheless, our new results show that one still obtains highly robust and `canonical' computability notions for a wide range of mathematical types arising in this way.

The talk will be high-level and aimed at a non-specialist audience. I will concentrate on the motivations for the work and on concrete mathematical examples, and will attempt a gentle introduction to the way in which the theorems in question are formulated, but will not go into their proofs.

A draft paper covering most of the material to be discussed is available at http://homepages.inf.ed.ac.uk/jrl/Research/ubiquity-reloaded3.pdf

SLIDES

1pm - 2:30pm LUNCH

2:30pm Invited Talk: Hazel Brickhill  (Bristol): Generalised Closed Unbounded and Stationary Sets  

The notions of closed unbounded and stationary set are central to Set Theory, and provide a way to measure how "large" or "thick" a subset of an ordinal is. In this talk I will introduce a generalisation of these notions, based on the generalisation of stationarity defined in [1]. Surprisingly for a new concept is set theory, generalised closed unbounded and stationary sets are very simple to define and accessible. They are closely related to the phenomena of stationary reflection and indescribability and can be characterised in terms of derived topologies [2],[3]. These notions are being used to answer questions about provability logic (see [2]), and promise a range of further applications.

[1] Bagaria, J., Magidor, M., and Sakai, H. (2015) "Reflection and indescribability in the constructible universe." Israel Journal of Mathematics 208.1: 1-11.

[2] L. Beklemishev, D. Gabelaia, (2014) "Topological interpretations of provability logic," Leo Esakia on duality in modal and intuitionistic logics, Outstanding Contributions to Logic, 4, eds. G. Bezhanishvili, Springer, 257–290

[3] Bagaria, J. (2016). "Derived topologies on ordinals and stationary reflection." "https://www.newton.ac.uk/files/preprints/ni16031.pdf

SLIDES

4pm Tea/Coffee

4:30pm Invited Talk: James Ladyman (Bristol) The Philosophical Logic of Homotopy Type Theory 

Homotopy Type Theory (HoTT) is a research programme in mathematics that connects algebraic topology with logic, computer science, and category theory. Its name derives from the way it integrates homotopy theory (which concerns spaces, points and paths) and formal type theory (as pioneered by Russell, Church, and Goedel, and developed in computer science) by interpreting types as spaces and terms of them as points in those spaces. Much of the interest in HoTT is due to the fact that it may be regarded as a `programming language for mathematics', and it is formulated in a way that facilitates automated computer proof checking. HoTT is a `foundation for mathematics' in the sense of a framework or language for mathematical practice. Within the language of HoTT it is possible to characterise mathematical structures such as natural numbers, real numbers, and groups, and to formalise proofs in homotopy theory.

However, philosophers often mean something stronger by `foundation for mathematics'. They require a foundation to provide not just a language but also a conceptual and epistemological basis for mathematics, and moreover one that can be formulated without relying upon any other existing foundation. HoTT is interesting for philosophers because of its putative foundational status in this sense. However, there are many other philosophically rich aspects to HoTT. One is the way identity is treated in the theory, which is extremely different from traditional approaches and is what makes the theory in one sense 'intensional'. Another is that the Univalence Axiom in HoTT arguably (and according to Steve Awodey) expresses mathematical structuralism. Further matters of interest are that the theory is constructive and the way this interacts with its other features. Finally, type theory in general, and dependent types in particular provide a different formal approach to functions and quantification, and a different way of dealing with predication.

I will present the basic ideas of HoTT paying particular attention to its novel conceptual foundations, and discussing a selection of philosophical issues in lesser and greater depth.

In this talk I will present the basic ideas of HoTT paying particular attention to its novel conceptual foundations, and discussing a selection of philosophical issues in lesser and greater depth.

SLIDES

5:30pm BLC Annual General Meeting

7:30pm Conference Dinner in Brighton

The dinner will be at the Sussex Yeoman conveniently located near to Brighton Station, the North Laine and central Brighton. Participants will need to travel to Birghton, ideally by train. Please purchase an off-peak return ticket Falmer-Brighton in advance if you stay on campus. Sussex Yeoman specialises in great locally and ethically sourced ingredients, won 'Best Sunday Roast 2014' in the Brighton and Hove Food & Drinks Awards, for their large selection of Sunday roasts with vegetarian, vegan and fish dishes being available. They also only use organic free range eggs from Mac’s Farm in Sussex. Dinner is pre-booked so if you want to join and have not registered, please contact the organisers.

Saturday 9th of September

9:30am Invited Talk: Tamara von Glehn (Cambridge): Games, traces and distributive laws 

Game semantics studies various categories of two-player games with strategies as morphisms. For simple games, composition of strategies can be viewed as taking a trace in a compact closed category. In this talk we will investigate how this can be extended to more complex notions of game, by considering the interaction of monads and comonads and lifting traced monoidal structure to their Kleisli categories and coalgebras. This is joint work in progress with Martin Hyland.

SLIDES

10:30am Richard Whyman (Leeds): How do we Describe the Computational Capabilities of an Arbitrary Physical System? l

Over the years various forms of physical computation whose method of computation is clearly distinct from that of the classic Turing machine model have been proposed and indeed utilised. Quantum computation being one of the most notable of these.

Various formalisms have already been proposed for describing in general how such physical systems compute . However, when it comes to describing what problems can be feasibly decided by these systems attention has typically focused on deriving complexity measures that only make sense in specific physical contexts. These measures are also typically incompatible with quantum computational complexity, which itself potentially falls short of providing reasonable complexity measures for physical systems that are even more computationally powerful than quantum computers, if such systems exist.

In this talk I shall present a new formalism for describing computation on an arbitrary physical system that avoids the time-dependent sequential algorithm and instead looks to the first-order theory of a given physical system for describing its decision capabilities. Computability-wise my new formalism suggests, as expected, that physical systems have the same decision capacity as Turing machines do. Complexity-wise this formalism gives the standard complexity classes for Turing machines and similar sequentially acting physical systems. However, the formalism also suggests that there are some physical systems which can, by going beyond the sequential algorithm, decide problems in $NP \cap co-NP$ rather than $P$, whilst utilising a polynomially bounded amount of resources.

Since factoring, the discrete logarithm and other problems that are feasibly computable by a quantum computer lie in $NP \cap co\text{-}NP$ our formalism potentially explains where the additional power of quantum computation is derived from.

SLIDES

11am Tea/Coffee

11:30am Invited Talk: Sam Staton (Oxford): Semantic models of higher-order probability theory

Bayesian statistics is full of interesting structure, particularly in its 'non-parametric' aspects. We have been working on semantic models for this structure from the perspective of probabilistic programming. For example, regression problems involve random functions, and we have built a new version of probability theory that allows probability measures over function spaces.

The talk will be based around recent papers in Proc. LICS and Proc. ESOP, partly in collaboration with Chris Heunen, Ohad Kammar, Frank Wood, Hongseok Yang and others.

SLIDES

12:30pm Andrew Brooke-Taylor (Leeds): Products of CW complexes: the full story 

CW complexes are the topological spaces of choice for much of algebraic topology, but the product of two CW complexes need not be a CW complex. Previous characterisations of when the product is a CW complex relied on making extra assumptions about the set-theoretic universe, such as CH. I will provide a complete characterisation of the circumstances under which the product of two CW complexes is a CW complex, valid without assuming any extra axioms; the characterisation involves the cardinal characteristic of the continuum b.

SLIDES 

1pm - 2:30pm LUNCH

2:30pm Uli Berger (Swansea): A concurrent computational interpretation of the law of excluded middle

We give a computational interpretation of the law of excluded middle as a scheme for the concurrent execution of processes. The interpretation, which takes place within the framework of realisability, involves two new logical operators: Set_n(A), allowing for n concurrent processes to realise the formula A, and A || B ('A restricted to B') which is realised by a computation that is guaranteed to terminate if A holds and, in case of termination, realises A.

We apply this interpretation to two examples of program extraction in computable analysis: Infinite Gray-code and matrix inversion via concurrent Gaussian elimination.

3pm Paulo Oliva (Queen Mary London): Modular Searching with Higher-order Functions

In this talk I’ll describe how some searching algorithms (from simple exhaustive search to alpha-beta prunning) can be done in a modular way using the continuation monad.

3:30pm END of MEETING