Bar recursion was invented by Spector to provide a proof of consistency for analysis via an extension of Gödel’s Dialectica interpretation to the axiom scheme of comprehension. Since then, several variants of this operator have been defined in various contexts, to provide computational content to diverse logical principles.

In this talk I will present various forms of bar recursion in the setting of the realizability and Dialectica interpretations. I will show how these operators give computational content to principles such as the double-negation shift, the axiom of choice in a classical setting, and the comprehension axiom of arithmetic.