System T and the Product of Selection Functions. - Martín Hötzel Escardó; Paulo Oliva; Thomas Powell 001 (CSL, 2011)

A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis - Paulo Oliva; Thomas Powell 001 (CoRR, 2012)

Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma - Thomas Powell 001 (CL&C, 2012)

On Spector's bar recursion. - Paulo Oliva; Thomas Powell 001 (Math. Log. Q., 2012)

On bar recursive interpretations of analysis. - Thomas Powell 001 (2013)

The equivalence of bar recursion and open recursion. - Thomas Powell 001 (Ann. Pure Appl. Log., 2014)

Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice. - Thomas Powell 001 (CoRR, 2014)

On the Computational Content of Termination Proofs. - Georg Moser; Thomas Powell 001 (CiE, 2015)

A constructive interpretation of Ramsey's theorem via the product of selection functions. - Paulo Oliva; Thomas Powell 001 (Math. Struct. Comput. Sci., 2015)

Gödel's functional interpretation and the concept of learning. - Thomas Powell 001 (LICS, 2016)

Bar recursion over finite partial functions. - Paulo Oliva; Thomas Powell 001 (Ann. Pure Appl. Log., 2017)

Well quasi-orders and the functional interpretation. - Thomas Powell 001 (CoRR, 2017)

A functional interpretation with state. - Thomas Powell 001 (LICS, 2018)

Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs. - Thomas Powell 001 (CoRR, 2018)

Sequential algorithms and the computational content of classical proofs. - Thomas Powell 001 (CoRR, 2018)

An Algorithmic Approach to the Existence of Ideal Objects in Commutative Algebra. - Thomas Powell 001; Peter Schuster 001; Franziskus Wiesnet (WoLLIC, 2019)

Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice. - Thomas Powell 001 (J. Log. Comput., 2019)

A proof-theoretic study of abstract termination principles. - Thomas Powell 001 (J. Log. Comput., 2019)

On the computational content of Zorn's lemma. - Thomas Powell 001 (LICS, 2020)

Dependent choice as a termination principle. - Thomas Powell 001 (Arch. Math. Log., 2020)

Rates of convergence for iterative solutions of equations involving set-valued accretive operators. - Ulrich Kohlenbach; Thomas Powell 001 (Comput. Math. Appl., 2020)

A computational interpretation of Zorn's lemma. - Thomas Powell 001 (CoRR, 2020)

A unifying framework for continuity and complexity in higher types. - Thomas Powell 001 (Log. Methods Comput. Sci., 2020)

A note on the finitization of Abelian and Tauberian theorems. - Thomas Powell 001 (Math. Log. Q., 2020)

A universal algorithm for Krull's theorem. - Thomas Powell 001; Peter Schuster 001; Franziskus Wiesnet (Inf. Comput., 2022)

A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory. - Thomas Powell 001 (Ann. Pure Appl. Log., 2023)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language. - Thomas Powell 001 (Log. Methods Comput. Sci., 2024)

Generalized Learnability of Stochastic Principles. - Morenikeji Neri; Nicholas Pischke; Thomas Powell 001 (CiE, 2025)