Thomas Powell Home ⚬ Papers ⚬ Talks ⚬ Teaching ⚬ CV

selected invited talks

• 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
• Type Theory, Constructive Mathematics and Geometric Logic (invited participant), CIRM, 1–5 May 2023
  Talk: Recursive inequalities in applied proof theory (slides, video)
• 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 (slides)
• Dagstuhl Seminar 22072: New Perspectives in Symbolic Computation and Satisfiability Checking, Schloss Dagstuhl, 13–18 February 2022
  Talk: Proof theory and computational algebra (slides)
• New Frontiers in Proofs and Computation, Banff International Research Station, 12–17 September 2021
  Talk (held online): A proof theoretic study of contractive mappings (slides)
• Logic Colloquium (Special Session on Proofs and Programs), Poznan; 19–24 July 2021
  Talk (held online): Some recent work in proof mining (slides)
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 9–13 November 2020
  Talk (held online): Quantitative Tauberian theorems (slides)
• 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 (slides)
• Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics, Mathematisches Forschungsinstitut Oberwolfach, 5–11 November 2017
  Talk: Functional interpretations with imperative features (slides)
• 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 (slides)
• Dagstuhl Seminar 16031: Well Quasi-Orders in Computer Science, Schloss Dagstuhl, 17–22 January 2016
  Talk: A constructive interpretation of open induction (slides)
• Continuity, Computability, Constructivity (CCC '15), Kochel, 14–18 September 2015
  Talk: Bar recursion over finite partial functions (slides)

lecture series

• Nordic Logic Summer School (NLS '22), University of Bergen, 13–16 June 2022
  Lecturer for the course Proof Mining (Lectures: 1, 2, 3, 4)
• 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 (course page)
• 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 (course page)

contributed talks, workshops & seminars

• 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 (slides)
• Structure vs Invariants in Proofs (StrIP) Kick-Off Workshop, University of Birmingham, 7–10 June 2022
  Talk: How Deep is the Dialectica? (slides)
• Theoretical Computer Science Seminar, University of Birmingham, 18 March 2022
  Talk: Recent results and open questions in applied proof theory (slides)
• Mathematical Logic Seminar, University of Lisbon, 7 February 2022
  Talk (held online): A proof theoretic analysis of Littlewood’s Tauberian theorem (slides)
• 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
• Minisymposium on Proof and Computation in Mathematics, DMV Annual Meeting, 14 September 2020
  Talk (held online): Some recent work in proof mining (slides)
• EECS Theory Seminar, Queen Mary University of London, 23 July 2020
  Talk (held online): Quantitative Tauberian theorems (slides)
• Logic in Computer Science (LICS '20), Saarland Informatics Campus (held online), 9 July 2020
  Talk (prerecorded): On the computational content of Zorn’s lemma (slides)
• 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 (slides)
• 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
• 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
• 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 (slides)
• Workshop: Proofs and Computation, Hausdorff Research Institute for Mathematics, Bonn, 2–6 July 2018
  Talk: Ideal objects and abstract machines (slides)
• Workshop on Computational Approaches to the Foundations of Mathematics, LMU Munich, 11–13 April 2018
  Talk: Ideal objects and abstract machines
• 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
• Mathematical Logic Seminar, LMU Munich, 12 July 2017
  Talk: Some applications of monads in proof theory (slides)
• Logic Research Seminar, University of Bern, 27 October 2016
  Talk: Learning, Loops and Limits (slides)
• Logic, Complexity and Automation, part of CLA '16, Obergurgl, 5–9 September 2016
  Talk: Complexity in Higher Types (slides)
• 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 (slides)
• Classical Logic and Computation (CL&C '16), Porto, 23 June 2016
  Talk: The computational content of Zorn's lemma (slides)
• 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
• 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 (slides)
• 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. (slides)
• Proof, Complexity and Verification Seminar, Swansea University, 4 December 2014
  Talk: The complexity of term rewrite systems (slides)
• 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 (slides)
• PLUME Seminar, ENS Lyon, 9 January 2014
  Talk: Bar recursive extensions of Gödel's system T (slides)
• 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 (slides)
• Theoretical Computer Science Seminar, University of Birmingham, 3 July 2012
  Talk: Modes of bar recursion (slides)
• 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 (slides)