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

Germany

- In summer semester 2019 I will be lecturing
*Higher Order Computability Theory*at TU Darmstadt. - I am an invited speaker at the special session
*Proof Theory and Proof Complexity*at this year's Logic Colloquium in Prague.

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.

**A unifying framework for continuity and complexity in higher types**

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

*Submitted, 2019.*[arXiv]**Dependent choice as a termination principle**

*Submitted, 2019.*[arxiv]**Sequential algorithms and the computational content of classical proofs**

*Submitted, 2018.*[arXiv]

**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]**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]**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]**Well quasi-orders and the functional interpretation**

*To appear in 'Well Quasi-Orders in Computation, Logic, Language and Reasoning', Trends in Logic, Springer.*[arXiv]**A functional interpretation with state**

*Proceedings of Logic in Computer Science (LICS 2018), IEEE Computer Society, 2018.*[preprint]**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.

**Computer Science Seminar**University of Verona, Italy.*20 March, 2019*

Talk: A new application of proof mining in the fixed point theory of uniformly convex Banach spaces**Invited Lecture Course**University of Verona, Italy.*15-20 March, 2019*

*Proof interpretations: A modern perspective***Autumn School on Proof and Computation**Fischbachau, Germany.*16-22 September, 2018*

Lecturer for the course*Proof Mining***European Summer School on Logic, Language and Information**Sofia University, Bulgaria.*6-17 August, 2018*

Lecturer for the course*Introduction to Proof Theory*with Anupam Das**Logic in Computer Science (LICS 2018)**University of Oxford, UK.*9-12 July, 2018*

Part of the Federated Logic Conference (FLoC 2018)

Talk: A functional interpretation with state**Workshop: Proofs and Computation**Hausdorff Research Institute for Mathematics, Bonn, Germany.*2-6 July, 2018*

Part of the Trimester Types, Sets and Constructions

Talk: Ideal objects and abstract machines**North American Summer School on Logic, Language and Information**Carnegie Mellon University, USA.*23-29 June, 2018*

Lecturer for the course*Proof Interpretations: A Modern Perspective*with Anupam Das**Workshop on Computational Approaches to the Foundations of Mathematics**LMU Munich, Germany.*11-13 April, 2018*

Talk: Ideal objects and abstract machines**Oberwolfach Workshop on Mathematical Logic: Proof Theory, Constructive Mathematics**MFO, Oberwolfach, Germany.*5-11 November, 2017*

Talk: Functional interpretations with imperative features**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)**Columbia University, 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.*