Thomas Powell


I am a postdoctoral researcher in mathematics, working 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. Well quasi-orders and the functional interpretation
    Submitted for publication. [arXiv]
  2. A proof theoretic study of abstract termination principles
    Submitted for publication. [arXiv]
  3. Spector bar recursion over finite partial functions
    with Paulo Oliva. Annals of Pure and Applied Logic 168(5):887-921, 2017. [arXiv]
  4. 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]
  5. Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
    Journal of Logic and Computation (advance access), 2015. [arXiv]
  6. On the computational content of termination proofs
    with Georg Moser. Proceedings of Computability in Europe (CiE 2015), LNCS 9136:276-285, 2015. [preprint]
  7. 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]
  8. 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]
  9. The equivalence of bar recursion and open recursion
    Annals of Pure and Applied Logic 165(11):1727-1754, 2014. [preprint]
  10. 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.
  11. On Spector's bar recursion
    with Paulo Oliva. Mathematical Logic Quarterly 58(4-5):356-365, 2012. [preprint]
  12. 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