1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 unknown
Modified bar recursion is a variant of Spector's bar recursion which can be used to give a realizability interpretation of the classical axiom of dependent choice. This realizability allows for the extraction of witnesses from proofs of forall-exists-formulas in classical analysis. In this talk I shall report on results regarding the relationship between modified and Spector's bar recursion. I shall also show that a seemingly weak form of modified bar recursion is as strong as "full" modified bar recursion in higher types.