Ordinal analysis of bar recursion of type zero

Howard, W. A.

Compositio Mathematica, Volume 42 (1980) p. 105-119

Functional interpretation of bar induction by bar recursion

Howard, W. A.

Compositio Mathematica, Volume 20 (1968) p. 107-124