Ordinal analysis of bar recursion of type zero
Compositio Mathematica, Tome 42 (1980) no. 1, p. 105-119 
@article{CM_1980__42_1_105_0,
     author = {Howard, W. A.},
     title = {Ordinal analysis of bar recursion of type zero},
     journal = {Compositio Mathematica},
     publisher = {Sijthoff et Noordhoff International Publishers},
     volume = {42},
     number = {1},
     year = {1980},
     pages = {105-119},
     zbl = {0444.03030},
     mrnumber = {594485},
     language = {en},
     url = {http://www.numdam.org/item/CM_1980__42_1_105_0}
}

Howard, W. A. Ordinal analysis of bar recursion of type zero. Compositio Mathematica, Tome 42 (1980) no. 1, pp. 105-119. http://www.numdam.org/item/CM_1980__42_1_105_0/

[1] H. Gerber: An extension of Schütte's Klammersymbols. Mathematische Annalen, 174 (1967), 203-216. | MR 223246 | Zbl 0162.01901

[2] H. Gerber, Brouwer's bar theorem and a system of ordinal notations. Proceedings of the Summer Conference on Intuitionism and Proof Theory. North-Holland, Amsterdam, 1970. | MR 280334 | Zbl 0205.01103

[3] W. Howard, Functional interpretation of bar induction by bar recursion. Compositio Mathematica 20 (1968) 107--124. | Numdam | MR 230619 | Zbl 0162.31503

[4] W. Howard, A system of abstract ordinals. Journal of Symbolic Logic, 37 (1972) 355-374. | MR 329869 | Zbl 0264.02026

[5] W. Howard, Ordinal analysis of terms of finite type, (to appear). | MR 583368 | Zbl 0444.03029

[6] W. Howard, Ordinal analysis of simple cases of bar recursion, (to appear). | MR 604874 | Zbl 0463.03031

[7] H. Vogel, Über die mit dem Bar-Rekursor vom Type 0 definierbaren Ordinalzahlen. Archiv für Mathematische Logik und Grundlagenforschung 19 (1978) 139-156. | MR 539870 | Zbl 0414.03034