Thomas Powell
Mathematician and Theoretical Computer Scientist


I am 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. A unifying framework for continuity and complexity in higher types
    Preprint, 2019. [arXiv]
  2. A proof theoretic study of abstract termination principles
    Submitted, 2019. [arXiv]
  3. Dependent choice as a termination principle
    Submitted, 2019. [arxiv]
  4. Sequential algorithms and the computational content of classical proofs
    Submitted, 2018. [arXiv]

Publications (peer reviewed)

  1. A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces
    To appear in Journal of Mathematical Analysis and Applications. [arXiv]
  2. An algorithmic approach to the existence of ideal objects in commutative algebra
    with Peter Schuster and Franziskus Wiesnet. To appear in Proceedings of WOLLIC, 2019. [arXiv]
  3. Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
    Chapter in Mathesis Universalis, Computability and Proof, ISBN 978-3-030-20446-4, Synthese Library, Springer, 2019. [arXiv]
  4. Well quasi-orders and the functional interpretation
    To appear in 'Well Quasi-Orders in Computation, Logic, Language and Reasoning', Trends in Logic, Springer. [arXiv]
  5. A functional interpretation with state
    Proceedings of Logic in Computer Science (LICS 2018), IEEE Computer Society, 2018. [preprint]
  6. Spector bar recursion over finite partial functions
    with Paulo Oliva. Annals of Pure and Applied Logic 168(5):887-921, 2017. [arXiv]
  7. 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]
  8. Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
    Journal of Logic and Computation (advance access), 2015. [arXiv]
  9. On the computational content of termination proofs
    with Georg Moser. Proceedings of Computability in Europe (CiE 2015), LNCS 9136:276-285, 2015. [preprint]
  10. 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]
  11. 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]
  12. The equivalence of bar recursion and open recursion
    Annals of Pure and Applied Logic 165(11):1727-1754, 2014. [preprint]
  13. 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.
  14. On Spector's bar recursion
    with Paulo Oliva. Mathematical Logic Quarterly 58(4-5):356-365, 2012. [preprint]
  15. 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