Royal Society International Scientific Seminar

Computational Interpretations of Mathematical Theorems

25 and 26 November 2013

Kavli Royal Society International Centre
Royal Society at Chicheley Hall
Newport Pagnell
Buckinghamshire MK16 9JJ
(direction to venue can be found here)

Aims and Scope

This two-day meeting brings together Mathematicians, Logicians and Computer Scientists with the aim of exploring novel connections between different research areas. The emphasis of the meeing is in the algorithmic content of mathematical proofs, an obvious point of intersection between Maths, Proof Theory and Computation.


Angus MacIntyre
Queen Mary University of London
Fernando Ferreira
Lisbon University
Genaro Lopez Acedo
Sevilla University
Grant Passmore
Cambridge University
Helmut Schwichtenberg
Ludwig-Maximilians University
Jeremy Avigad
Carnegie Mellon University
Marcelo Fiore
Cambridge University
Mark Pollicott
University of Warwick
Martin Escardo
Birmigham University
Monika Seisenberger
Swansea University
Oscar Bandtlow
Queen Mary University of London
Paulo Oliva
Queen Mary University of London
Peter Paule
Research Institute for Symbolic Computation
Rafael Espinola Garcia
Sevilla University
Rob Arthan
Queen Mary University of London / Lemma1 Ltd
Robert Simon
London School of Economics
Steve Simpson
Pennsylvania State University
Thierry Coquand
Goetenborg University
Thomas Ward
University of East Anglia
Ulrich Berger
Swansea University
Ulrich Kohlenbach
Darmstadt University

Program: Monday 25 November

09:00 - 09:15 Opening
09:15 - 10:00 Angus MacIntyre: Unwinding in the style of Kreisel: The Case of Littlewood's Theorem (abstract)
10:00 - 10:45 Ulrich Kohlenbach: Proof mining (abstract)
10:45 - 11:15 Coffee break
11:15 - 12:00 Genaro Lopez-Acedo: Metric fixed point theory (abstract)
12:00 - 12:45 Oscar Bandtlow: Approximation of invariant measures for chaotic dynamical systems (abstract)
12:45 - 14:00 Lunch
14:00 - 14:45 Mark Pollicott: Computation of the dimensions of fractals (abstract)
14:45 - 15:30 Thomas Ward: Towards a Polya-Carlson dichotomy in algebraic dynamics (abstract)
15:30 - 16:00 Coffee break
16:00 - 17:00 Martin Escardo: Topology and computation (abstract)

Program: Tuesday 26 November

09:00 - 09:45 Jeremy Avigad: Computability and uniformity in ergodic theory (abstract)
09:45 - 10:30 Robert Simon: Ergodic theory and games of incomplete information (abstract)
10:30 - 11:15 Coffee break
11:15 - 12:00 Thierry Coquand: A cubical set model for the Univalent Foundation (abstract)
12:00 - 12:45 Steve Simpson: Recursion theory and symbolic dynamics (abstract)
12:45 - 14:00 Lunch
14:00 - 14:45 Ulrich Berger: Program extraction (abstract)
14:45 - 15:30 Marcelo Fiore: Universal algebra for computational calculi (abstract)
15:30 - 16:00 Coffee break
16:00 - 17:00 Peter Paule: Symbolic computation, combinatorics, and modular forms (abstract)

Last updated 24 Oct 2013 (Paulo Oliva)