Thomas Powell
Mathematician and Theoretical Computer Scientist


I a postdoctoral researcher in the Logic Group of the Department of Mathematics at the Technische Universität Darmstadt.

Previously I held a postdoctoral position in the Computational Logic group at the University of Innsbruck, and a CARMIN research fellowship at the Institut des Hautes Études Scientifiques. I obtained my PhD from Queen Mary University of London.

For more information see my curriculum vitae.

Email: powell AT mathematik DOT tu-darmstadt DOT de

Tel: (+49)06151-16-22844

Office: S2|15-226

Address: Fachbereich Mathematik
Schlossgartenstraße 7
64289 Darmstadt



My main area of research is mathematical logic and proof theory. More specifically I focus on topics related to functional interpretations, including the extraction of computational content from proofs and higher type computability theory. I am particularly interested in applications of proof theoretic techniques, in both mathematics and computer science.


  1. An algorithmic approach to the existence of ideal objects in commutative algebra
    with Peter Schuster and Franziskus Wiesnet. Preprint, 2019. [arXiv]
  2. A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces
    Preprint, 2019. [arXiv]
  3. A proof theoretic study of abstract termination principles
    Preprint, 2019. [arXiv]
  4. Dependent choice as a termination principle
    Preprint, 2019. [arxiv]
  5. Sequential algorithms and the computational content of classical proofs
    Preprint, 2018. [arXiv]
  6. Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
    To appear in 'Mathesis Universalis, Computability and Proof', Synthese Library, Springer. [arXiv]
  7. A functional interpretation with state
    Proceedings of Logic in Computer Science (LICS 2018), IEEE Computer Society, 2018. [preprint]
  8. Well quasi-orders and the functional interpretation
    To appear in 'Well Quasi-Orders in Computation, Logic, Language and Reasoning', Trends in Logic, Springer. [arXiv]
  9. Spector bar recursion over finite partial functions
    with Paulo Oliva. Annals of Pure and Applied Logic 168(5):887-921, 2017. [arXiv]
  10. Gödel's functional interpretation and the concept of learning
    Proceedings of Logic in Computer Science (LICS 2016), IEEE Computer Society, 136-145, 2016. [preprint]
  11. Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
    Journal of Logic and Computation (advance access), 2015. [arXiv]
  12. On the computational content of termination proofs
    with Georg Moser. Proceedings of Computability in Europe (CiE 2015), LNCS 9136:276-285, 2015. [preprint]
  13. A game-theoretic computational interpretation of proofs in classical analysis
    with Paulo Oliva. Chapter in Gentzen's Centenary: The Quest for Consistency, ISBN 978-3-319-10102-6, Springer, 2015. [arXiv]
  14. A constructive interpretation of Ramsey's theorem via the product of selection functions
    with Paulo Oliva. Mathematical Structures in Computer Science 25(8):1755-1778, 2015. [arXiv]
  15. The equivalence of bar recursion and open recursion
    Annals of Pure and Applied Logic 165(11):1727-1754, 2014. [preprint]
  16. Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's Lemma
    Proceedings of Classical Logic and Computation (CL&C 2012), EPTCS 97:49-62, 2012.
  17. On Spector's bar recursion
    with Paulo Oliva. Mathematical Logic Quarterly 58(4-5):356-365, 2012. [preprint]
  18. System T and the product of selection functions
    with Martín Escardó and Paulo Oliva. Proceedings of Computer Science Logic (CSL 2011), LIPIcs 12:233-247, 2011.

Technical reports


Here are slides from some talks I've given, along with details of meetings I have, or will be attending.

Other events