Thomas Powell Home ⚬ Papers ⚬ Events ⚬ CV

upcoming events

• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 15–20 November 2026
• Second Workshop on Proof Mining, University of Bath, 7–9 September 2026.
• Logic Colloquium, Swansea University, 29 June– 3 July 2026

past events and talks

• Seminário de Lógica Matemática, University of Lisbon, 2 March 2026
  Talk: Applications of proof theory in probability and stochastic optimization
• Types and Topology: A workshop in honour of Martín Escardó's 60th birthday, University of Birmingham, 17–18 December 2025
  Talk: Applications of proof theory in probability and stochastic optimization
• International Workshop on Programs from Proofs, University of Bath, 15–16 September 2025
  Talk: On proof theoretic and quantitative aspects of stochastic processes
• Topos Institute Colloquium, 16 October 2024
  Talk: Quantitative results for stochastic processes (video)
• Theory seminar, Swansea University, 12 September 2024
  Talk: Rates of convergence for stochastic processes
• Workshop on Proof Mining 2024, TU Darmstadt, 4–6 September 2024
  Talk: Rates of convergence for stochastic processes
• Mathematical Colloquium, TU Darmstadt, 17 July 2024
  Talk: Quantitative results for stochastic processes
• 40th British Colloquium for Theoretical Computer Science, (organiser), University of Bath, 4–5 April 2024
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 12–17 November 2023
  Talk: New applications of proof theory: Greedy algorithms, probability, and proof assistants
• Working Formal Methods Symposium (FROM '23), Bucharest, 21&ndash'22 September 2023
• Type Theory, Constructive Mathematics and Geometric Logic (invited participant), CIRM, 1–5 May 2023
  Talk: Recursive inequalities in applied proof theory (video)
• Mathematical Foundations of AI seminar, Queen Mary University of London, 2 February 2023
  Talk: A brief overview of applied proof theory, and some ideas for where it might be going next
• International Conference on Applied Proof Theory 2022, Pescara, 29 August – 2 September 2022
  Talk: Personal reflections on becoming an applied proof theorist, and thoughts for the future
• Nordic Logic Summer School (NLS '22), University of Bergen, 13–16 June 2022
  Lecturer for the course Proof Mining
• Structure vs Invariants in Proofs (StrIP) Kick-Off Workshop, University of Birmingham, 7–10 June 2022
  Talk: How Deep is the Dialectica?
• Theoretical Computer Science Seminar, University of Birmingham, 18 March 2022
  Talk: Recent results and open questions in applied proof theory
• Dagstuhl Seminar 22072: New Perspectives in Symbolic Computation and Satisfiability Checking, Schloss Dagstuhl, 13–18 February 2022
  Talk: Proof theory and computational algebra
• Mathematical Logic Seminar, University of Lisbon, 7 February 2022
  Talk (held online): A proof theoretic analysis of Littlewood’s Tauberian theorem
• New Frontiers in Proofs and Computation, Banff International Research Station, 12–17 September 2021
  Talk (held online): A proof theoretic study of contractive mappings
• Logic Colloquium (Special Session on Proofs and Programs), Poznan; 19–24 July 2021
  Talk (held online): Some recent work in proof mining
• Computer Science Colloquium, Augusta University, 16 April 2021
  Talk (held online): Quantitative Tauberian theorems
• Logic and Verification Seminar, Laboratoire d'Informatique de Paris Nord, 25 November 2020
  Talk (held online): Quantitative Tauberian theorems
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 9–13 November 2020
  Talk (held online): Quantitative Tauberian theorems
• Minisymposium on Proof and Computation in Mathematics, DMV Annual Meeting, 14 September 2020
  Talk (held online): Some recent work in proof mining
• EECS Theory Seminar, Queen Mary University of London, 23 July 2020
  Talk (held online): Quantitative Tauberian theorems
• Logic in Computer Science (LICS '20), Saarland Informatics Campus (held online), 9 July 2020
  Talk: On the computational content of Zorn’s lemma (video)
• Theoretical Computer Science Seminar, University of Birmingham, 12 June 2020
  Talk (held online): Quantitative Tauberian theorems
• Mathematical Foundations Seminar, University of Bath, 12 May 2020
  Talk (held online): Quantitative Tauberian theorems
• Algebra and Algorithms, Djerba, 4–6 February 2020
  Talk: Gödel's functional interpretation in constructive algebra
• Logik-Arbeitstagung Bern, München und Verona, LMU Munich, 12–13 November 2019
  Talk: A new application of proof mining in the fixed point theory of uniformly convex Banach spaces
• Logic Colloquium (Special Session on Proof Theory and Proof Complexity), Prague, 11–16 August 2019
  Talk: A new application of proof mining in the fixed point theory of uniformly convex Banach spaces
• Computer Science Seminar, University of Verona, 20 March 2019
  Talk: A new application of proof mining in the fixed point theory of uniformly convex Banach spaces
• Invited Lecture Course, University of Verona, 15–20 March 2019
  Lecturer for the course Proof Interpretations: A Modern Perspective
• Autumn School on Proof and Computation, Fischbachau, 16–22 September 2018
  Lecturer for the course Proof Mining
• European Summer School on Logic, Language and Information (ESSLLI '18), Sofia University, 6–17 August 2018
  Lecturer for the course Introduction to Proof Theory with Anupam Das
• Logic in Computer Science (LICS '18), part of the Federated Logic Conference (FLoC '18), University of Oxford, 9–12 July 2018
  Talk: A functional interpretation with state
• Workshop: Proofs and Computation, Hausdorff Research Institute for Mathematics, Bonn, 2–6 July 2018
  Talk: Ideal objects and abstract machines
• North American Summer School on Logic, Language and Information (NASSLLI '18), Carnegie Mellon University, 23–29 June 2018
  Lecturer for the course Proof Interpretations: A Modern Perspective with Anupam Das
• Workshop on Computational Approaches to the Foundations of Mathematics, LMU Munich, 11–13 April 2018
  Talk: Ideal objects and abstract machines
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 5–11 November 2017
  Talk: Functional interpretations with imperative features
• Minisymposium on Applied Proof Theory and the Computational Content of Mathematics, Joint ÖMG and DMV Congress, Salzburg, 14 September 2017
  Talk: Proof interpretations with imperative features
• Humboldt-Kolleg: Proof Theory as Mathesis Universalis, Villa Vigoni, Como, 24–27 July 2017
  Talk: Gödel's functional interpretation and the extraction of imperative programs from proofs
• Mathematical Logic Seminar, LMU Munich, 12 July 2017
  Talk: Some applications of monads in proof theory
• Logic Research Seminar, University of Bern, 27 October 2016
  Talk: Learning, Loops and Limits
• Logic, Complexity and Automation, part of CLA '16, Obergurgl, 5–9 September 2016
  Talk: Complexity in Higher Types
• Logic in Computer Science (LICS '16), Columbia University, New York City, 5–8 July 2016
  Talk: Gödel's functional interpretation and the concept of learning
• Classical Logic and Computation (CL&C '16), Porto, 23 June 2016
  Talk: The computational content of Zorn's lemma
• Mathematics for Computation, Niederalteich, 8–13 May 2016
  Talk: Gödel's functional interpretation and higher order learning
• Proof, Computational, Complexity (PCC 2016), Munich, 5–6 May 2016
  Talk: The computational content of Zorn's lemma
• Dagstuhl Seminar 16031: Well Quasi-Orders in Computer Science, Schloss Dagstuhl, 17–22 January 2016
  Talk: A constructive interpretation of open induction
• Workshop on Efficient and Natural Proof Systems, University of Bath, 14–16 December 2015
  Talk: Gödel's functional interpretation and the concept of learning
• Mathematical Logic Seminar, LMU Munich, 4 November 2015
  Talk: Learning procedures arising from Gödel's functional interpretation
• Continuity, Computability, Constructivity (CCC '15), Kochel, 14–18 September 2015
  Talk: Bar recursion over finite partial functions
• Computability in Europe (CiE '15), Bucharest, 29 June–3 July 2015
  Talk: On the computational content of termination proofs
• Epsilon 2015, University of Montpellier, 10–12 June 2015
  Talk: Variations on learning: Relating the epsilon calculus to proof interpretations.
• Proof, Complexity and Verification Seminar, Swansea University, 4 December 2014
  Talk: The complexity of term rewrite systems
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 16–22 November 2014
• Second Workshop on the Two Faces of Complexity, Vienna Summer of Logic, 12 July 2014
  Talk: Proof theoretic approaches to rewriting
• Thematic Trimester on the Semantics of Proofs and Certified Mathematics, IHP, Paris, 7 April–11 July 2014
  preceded by Summer Pre-School at CIRM, Marseille, 7–18 April
• Séminaire de Mathématiques, IHÉS, 14 January 2014
  Talk: Applications of proof interpretations in mathematics
• PLUME Seminar, ENS Lyon, 9 January 2014
  Talk: Bar recursive extensions of Gödel's system T
• Proof, Complexity and Verification Seminar, Swansea University, 18 December 2013
  Talk: Bar recursive extensions of Gödel's system T
• Semantics Seminar, PPS lab, Université Paris Diderot, 12 November 2013
  Talk: Bar recursive extensions of Gödel's system T
• Workshop on Classical Logic and Computation (CL&C '12), University of Warwick, 8 July 2012
  Talk: A constructive proof of Higman's lemma
• Theoretical Computer Science Seminar, University of Birmingham, 3 July 2012
  Talk: Modes of bar recursion
• International Spring School on the Formalisation of Mathematics, INRIA, Sophia-Antipolis, 12–16 March 2012
  
• Computer Science Logic (CSL '11), Bergen, 12–15 September 2011
  Talk: System T and the product of selection functions
• Joint Queen Mary/Imperial Seminar, Queen Mary University of London, 7 September 2011
  Talk: System T and the product of selection functions