Royal Society International Scientific Seminar Interpretations of Mathematical Theorems (original) (raw)
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.
Participants
| 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)