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

- I am co-organiser, together with Sam Sanders, of the minisymposium Applied Proof Theory and the Computational Content of Mathematics, which will take place on 14th September in Salzburg as part of this year's joint congress of the Österreichische Mathematische Gesellschaft (ÖMG) and Deutsche Mathematiker-Vereinigung (DMV).
- I will give a talk at the Humboldt Kolleg event
*Proof Theory as Mathesis Universalis*which will take place from 24th to 28th July at Villa Vigoni in Loveno di Menaggio, Como. - In July I will visit LMU Munich and give a talk in the Mathematical Logic Seminar.
- 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**

*Submitted for publication.*[arXiv]**A proof theoretic study of abstract termination principles**

*Submitted for publication.*[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***Humboldt-Kolleg: Proof Theory as Mathesis Universalis**Villa Vigoni, Como, Italy*24-27 July, 2017.***Mathematical Logic Seminar**Ludwig-Maximilians-Universität, Munich, Germany.*12 July, 2017*

**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.*