Thomas Powell Home ⚬ Papers ⚬ Events ⚬ CV

The arXiv contains some but not all of my papers, and these sometimes differ from the final published manuscript, so it's better to consult the versions indicated below.

preprints

  1. Convergence guarantees for stochastic algorithms solving non-unique problems in metric spaces
    Nicholas Pischke and Thomas Powell
    (arXiv) Submitted.
  2. An abstract effective convergence theorem for stochastic processes, with applications to stochastic approximation
    Morenikeji Neri, Nicholas Pischke and Thomas Powell
    (arXiv) Submitted.
  3. Generalized fluctuation bounds for stochastic algorithms in the presence of compactness
    Morenikeji Neri, Nicholas Pischke and Thomas Powell
    (arXiv) Submitted.
  4. An approximate zero-one law via the Dialectica interpretation
    Thomas Powell and Alex Wan
    (arXiv) Submitted.

peer reviewed

  1. Proof mining and high-level proof theoretic reasoning: A case study on greedy approximation schemes
    Thomas Powell
    (doi, pdf) Bulletin of Symbolic Logic (2026+).
  2. Asymptotic regularity of a generalised stochastic Halpern scheme with applications
    Nicholas Pischke and Thomas Powell
    (doi, arXiv) Journal of Optimization Theory and Applications 210, 3 (2026).
  3. On the algorithmic structure of Dialectica realisers
    Davide Barbarossa and Thomas Powell
    (doi, arXiv) Proceedings of CSL '26, LIPIcs 363: 22:1–22:22 (2026).
  4. A quantitative Robbins-Siegmund theorem
    Morenikeji Neri and Thomas Powell
    (doi, arXiv) Annals of Applied Probability 36(1): 636–651 (2026).
  5. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales
    Morenikeji Neri and Thomas Powell
    (doi, arXiv) Transactions of the American Mathematical Society, Series B 12: 974–1019, (2025).
  6. Generalized learnability of stochastic principles
    Morenikeji Neri, Nicholas Pischke and Thomas Powell
    (doi, pdf) Proceedings of CiE '25, LNCS 15764: 333–348 (2025).
  7. Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
    Thomas Powell
    (doi, arXiv) Logical Methods in Computer Science 20(1): 7:1–7:32 (2024).
  8. A computational study of a class of recursive inequalities
    Morenikeji Neri and Thomas Powell
    (doi, arXiv) Journal of Logic and Analysis 15(3): 1–48 (2023).
  9. A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory
    Thomas Powell
    (doi, pdf) Annals of Pure and Applied Logic 174(4): 103231 (2023).
  10. A universal algorithm for Krull's theorem
    Thomas Powell, Peter Schuster and Franziskus Wiesnet
    (doi, pdf) Information and Computation 287: 104761 (2022).
  11. Rates of convergence for asymptotically weakly contractive mappings in normed spaces
    Thomas Powell and Franziskus Wiesnet
    (doi, pdf) Numerical Functional Analysis and Optimization 42(15): 1802–1838 (2021).
  12. A note on the finitization of Abelian and Tauberian theorems
    Thomas Powell
    (doi, pdf) Mathematical Logic Quarterly 66(3): 300–310 (2020).
  13. A unifying framework for continuity and complexity in higher types
    Thomas Powell
    (doi, arXiv) Logical Methods in Computer Science 16(3): 17:1–17:28 (2020).
  14. On the computational content of Zorn's lemma
    Thomas Powell
    (doi, pdf) Proceedings of LICS '20: 768–781, ACM (2020).
  15. Rates of convergence for iterative solutions of equations involving set-valued accretive operators
    Ulrich Kohlenbach and Thomas Powell
    (doi, arXiv) Computers & Mathematics with Applications 80(3): 490–503 (2020).
  16. Dependent choice as a termination principle
    Thomas Powell
    (doi, pdf) Archive for Mathematical Logic 59(3–4): 503–516 (2020).
  17. Well quasi-orders and the functional interpretation
    Thomas Powell
    (doi, pdf) Chapter in Well Quasi-Orders in Computation, Logic, Language and Reasoning, Trends in Logic 53: 221–269, Springer (2020).
  18. A proof theoretic study of abstract termination principles
    Thomas Powell
    (doi, pdf) Journal of Logic and Computation 29(8): 1345–1366 (2019).
  19. Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
    Thomas Powell
    (doi, pdf) Chapter in Mathesis Universalis, Computability and Proof, Synthese Library 412: 255–290, Springer (2019).
  20. A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces
    Thomas Powell
    (doi, arXiv) Journal of Mathematical Analysis and Applications 478(2): 790–805 (2019).
  21. Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
    Thomas Powell
    (doi, arXiv) Journal of Logic and Computation 29(4): 519–554 (2019).
  22. An algorithmic approach to the existence of ideal objects in commutative algebra
    Thomas Powell, Peter Schuster and Franziskus Wiesnet
    (doi, pdf) Proceedings of WoLLIC '19, LNCS 11541: 533–549 (2019).
  23. A functional interpretation with state
    Thomas Powell
    (doi, pdf) Proceedings of LICS '18: 839–848, ACM (2018).
  24. Bar recursion over finite partial functions
    Paulo Oliva and Thomas Powell
    (doi, arXiv) Annals of Pure and Applied Logic 168(5): 887–921 (2017).
  25. Gödel's functional interpretation and the concept of learning
    Thomas Powell
    (doi, pdf) Proceedings of LICS '16: 136–145, ACM (2016).
  26. On the computational content of termination proofs
    Georg Moser and Thomas Powell
    (doi, pdf) Proceedings of CiE '15, LNCS 9136: 276–285 (2015).
  27. A game-theoretic computational interpretation of proofs in classical analysis
    Paulo Oliva and Thomas Powell
    (doi, arXiv) Chapter in Gentzen's Centenary: The Quest for Consistency: 501–531, Springer (2015).
  28. A constructive interpretation of Ramsey's theorem via the product of selection functions
    Paulo Oliva and Thomas Powell
    (doi, arXiv) Mathematical Structures in Computer Science 25(8): 1755–1778 (2015).
  29. The equivalence of bar recursion and open recursion
    Thomas Powell
    (doi, pdf) Annals of Pure and Applied Logic 165(11): 1727–1754 (2014).
  30. Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's Lemma
    Thomas Powell
    (doi) Proceedings of CL&C '12, EPTCS 97: 49–62 (2012).
  31. On Spector's bar recursion
    Paulo Oliva and Thomas Powell
    (doi) Mathematical Logic Quarterly 58(4–5): 356–365 (2012).
  32. System T and the product of selection functions
    Martín Escardó, Paulo Oliva and Thomas Powell
    (doi) Proceedings of CSL '11, LIPIcs 12: 233–247 (2011).

other

phd thesis