Title: On variants of modified bar recursion 

Paulo Oliva and Martin Escardo
 

In 1962 Spector showed how the Dialectica interpretation of the
classical countable choice can be witnessed by a higher order
recursion on well-founded trees, so-called bar recursion. More
recently, in 1998, Berardi/Bezem/Coquand showed how a variant of bar
recursion can be used to interpret the classical countable choice via
a form of realizability interpretation. Let us call the recursion
schema used by them the BBC functional. Their work was soon after
simplified by Ulrich Berger, who showed how the standard modified
realizability (due to Kreisel) could be used when combined with what
he called "modified bar recursion", MBR for short.  In this talk I
will discuss a third variant of modified bar recursion, which arose
from recent work of Martin Escardo, and seems to be more efficient
than MBR and is easier to work with than BBC. In particular, I will
show that Escardo's bar recursion (which we call course-of-value bar
recursion CBR due to the combination of course-of-value induction and
bar recursion) is primitive recursively equivalent to Berger's
modified bar recursion.