Thomas Powell Home ⚬ Papers ⚬ Talks ⚬ Teaching ⚬ CV

My entire research output is open access, through publication in an open access journal or via an author accepted manuscript made publicly available here. 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. Proof mining and informal proof theoretic reasoning: A case study on greedy approximation schemes
    Thomas Powell
    (pdf) Preprint, 2023.

peer reviewed

  1. 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.
  2. 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.
  3. 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.
  4. A universal algorithm for Krull's theorem
    Thomas Powell, Peter Schuster and Franziskus Wiesnet
    (doi, pdf) Information and Computation, 287: 104761, 2022.
  5. 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.
  6. A note on the finitization of Abelian and Tauberian theorems
    Thomas Powell
    (doi, pdf) Mathematical Logic Quarterly, 66(3): 300–310, 2020.
  7. 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.
  8. On the computational content of Zorn's lemma
    Thomas Powell
    (doi, pdf) Proceedings of LICS '20, pp. 768–781, ACM, 2020.
  9. 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
  10. Dependent choice as a termination principle
    Thomas Powell
    (doi, pdf) Archive for Mathematical Logic, 59(3–4): 503–516, 2020
  11. 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
  12. A proof theoretic study of abstract termination principles
    Thomas Powell
    (doi, pdf) Journal of Logic and Computation, 29(8): 1345–1366, 2019
  13. 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
  14. 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
  15. 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
  16. 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
  17. A functional interpretation with state
    Thomas Powell
    (doi, pdf) Proceedings of LICS '18, pp. 839–848, ACM, 2018
  18. Bar recursion over finite partial functions
    Paulo Oliva and Thomas Powell
    (doi, arXiv) Annals of Pure and Applied Logic, 168(5): 887–921, 2017
  19. Gödel's functional interpretation and the concept of learning
    Thomas Powell
    (doi, pdf) Proceedings of LICS '16, pp. 136–145, ACM, 2016
  20. On the computational content of termination proofs
    Georg Moser and Thomas Powell
    (doi, pdf) Proceedings of CiE '15, LNCS 9136: 276–285, 2015
  21. 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, pp. 501–531, Springer, 2015
  22. 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
  23. The equivalence of bar recursion and open recursion
    Thomas Powell
    (doi, pdf) Annals of Pure and Applied Logic, 165(11): 1727–1754, 2014
  24. 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
  25. On Spector's bar recursion
    Paulo Oliva and Thomas Powell
    (doi) Mathematical Logic Quarterly, 58(4–5): 356–365, 2012
  26. 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