The bounded functional interpretation of bar induction

Relying on the extension of the bounded functional interpretation to bar recursive functionals of finite type, we prove that the scheme of bar induction has a bounded functional interpretation via bar recursors. As a consequence, the axiom of dependent choices also has a bounded functional interpretation.