Modified bar recursion
Ulrich Berger, Paulo B. Oliva · Mathematical Structures in Computer Science · 2006
This paper studies modified bar recursion, a higher type recursion scheme, which has been used in Berardi et al. (1998) and Berger and Oliva (2005) for a realisability interpretation of classical analysis. A complete clarification of its relation to Spector's and Kohlenbach's bar recursion, the fan functional, Gandy's functional and Kleene's notion of S1–S9 computability is given.