The herbrand functional interpretation of the double negation shift

This paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type J_R^TX =(X → R)→ TX . It is assumed throughout that R is a T-algebra. We show that J_R^T is also a strong monad, and that it embeds into the continuation monad K_RX =(X → R)→ R. We use this to derive that the explicitly controlled product of T-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when T is the finite powerset monad P_f(·). These are used to show that when TX = P_f (X) the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.