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

Germany

- Together with Anupam Das I will give the Foundational Course
*Introduction to Proof Theory*at ESSLLI 2018 in Sofia, Bulgaria. - Preprints of two new papers can now be found on the arXiv, one on a proof theoretic analysis of termination (here), and the other on the functional interpretation of results in well quasi-order theory (here).

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.

**Well quasi-orders and the functional interpretation**

*Preprint.*[arXiv]**A proof theoretic study of abstract termination principles**

*Preprint.*[arXiv]**Spector bar recursion over finite partial functions**

with Paulo Oliva.*Annals of Pure and Applied Logic 168(5):887-921, 2017.*[arXiv]**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]**Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice**

*Journal of Logic and Computation (advance access), 2015.*[arXiv]**On the computational content of termination proofs**

with Georg Moser.*Proceedings of Computability in Europe (CiE 2015), LNCS 9136:276-285, 2015.*[preprint]**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]**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]**The equivalence of bar recursion and open recursion**

*Annals of Pure and Applied Logic 165(11):1727-1754, 2014.*[preprint]**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.***On Spector's bar recursion**

with Paulo Oliva.*Mathematical Logic Quarterly 58(4-5):356-365, 2012.*[preprint]**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.*

**On Bar Recursive Interpretations of Analysis**

PhD dissertation, Queen Mary University of London, August 2013.

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

**Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics**MFO, Oberwolfach, Germany.*5-11 November, 2017*

**Minisymposium on Applied Proof Theory and the Computational Content of Mathematics**Joint ÖMG and DMV Congress, Salzburg, Austria.*14 September, 2017*

Talk: Proof interpretations with imperative features**Humboldt-Kolleg: Proof Theory as Mathesis Universalis**Villa Vigoni, Como, Italy*24-27 July, 2017*

Talk Gödel's functional interpretation and the extraction of imperative programs from proofs**Mathematical Logic Seminar**Ludwig-Maximilians-Universität, Munich, Germany.*12 July, 2017*

Talk: Some applications of monads in proof theory**Logic Research Seminar**University of Bern, Switzerland.*27 October, 2016*

Talk: Learning, Loops and Limits**Logic, Complexity and Automation**, part of CLA 2016, Obergurgl, Austria.*5-9 September, 2016*

Talk: Complexity in Higher Types**Logic in Computer Science (LICS 2016)**New York City, USA.*5-8 July, 2016*

Talk: Gödel's functional interpretation and the concept of learning**Classical Logic and Computation (CL&C 16)**Porto, Portugal.*23 June, 2016*

Talk: The computational content of Zorn's lemma**Mathematics for Computation**Niederalteich, Germany.*8-13 May, 2016*

Talk: Gödel's functional interpretation and higher order learning**Proof, Computational, Complexity (PCC 2016)**Munich, Germany.*5-6 May, 2016*

Talk: The computational content of Zorn's lemma**Dagstuhl Seminar 16031: Well Quasi-Orders in Computer Science**Schloss Dagstuhl, Germany.*17-22 January, 2016*

Talk: A constructive interpretation of open induction**Workshop on Efficient and Natural Proof Systems**University of Bath, UK.*14-16 December, 2015*

Talk: Gödel's functional interpretation and the concept of learning**Mathematical Logic Seminar**Ludwig-Maximilians-Universität, Munich, Germany.*4 November, 2015*

Talk: Learning procedures arising from Gödel's functional interpretation**Continuity, Computability, Constructivity (CCC 2015)**(invited speaker) Kochel, Germany.*14-18 September, 2015*

Talk: Bar recursion over finite partial functions**Computability in Europe (CiE 2015)**Bucharest, Romania.*29 June - 3 July, 2015*

Talk: On the computational content of termination proofs**Epsilon 2015**University of Montpellier, France.*10-12 June, 2015*

Talk: Variations on learning: Relating the epsilon calculus to proof interpretations.**Proof, Complexity and Verification Seminar**Swansea University, UK.*4 December, 2014*

Talk: The complexity of term rewrite systems**Second Workshop on the Two Faces of Complexity**(invited speaker), part of Vienna Summer of Logic, Austria.*12 July 2014*

Talk: Proof theoretic approaches to rewriting**Séminaire de Mathématiques**IHÉS, France.*14 January, 2014*

Talk: Applications of proof interpretations in mathematics**PLUME Seminar**ENS Lyon, France.*9 January, 2014*

Talk: Bar recursive extensions of Gödel's system T**Proof, Complexity and Verification Seminar**Swansea University, UK.*18 December 2013*

Talk: Bar recursive extensions of Gödel's system T**Semantics Seminar, PPS lab**Université Paris Diderot, France.*12 November 2013*

Talk: Bar recursive extensions of Gödel's system T**Fourth International Workshop on Classical Logic and Computation (CL&C 2012)**University of Warwick, UK.*8 July 2012*

Talk: A constructive proof of Higman's lemma**Theoretical Computer Science Seminar**University of Birmingham, UK.*3 July 2012*

Talk: Modes of bar recursion**Computer Science Logic (CSL 2011)**Bergen, Norway.*12-15 September 2011*

Talk: System T and the product of selection functions

**Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics**MFO, Oberwolfach, Germany.*16-22 November, 2014.***Thematic Trimester on the Semantics of Proofs and Certified Mathematics**IHP, Paris, France.*7 April - 11 July, 2014.*

along with Summer Pre-School at CIRM, Marseille,*7-18 April.***International Spring School on the Formalisation of Mathematics**INRIA, Sophia-Antipolis, France.*12-16 March, 2012.*