Ordinal analysis of bar recursion of type zero
Compositio Mathematica, Tome 42 (1980) no. 1, pp. 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},
     pages = {105--119},
     publisher = {Sijthoff et Noordhoff International Publishers},
     volume = {42},
     number = {1},
     year = {1980},
     mrnumber = {594485},
     zbl = {0444.03030},
     language = {en},
     url = {http://www.numdam.org/item/CM_1980__42_1_105_0/}
}
TY  - JOUR
AU  - Howard, W. A.
TI  - Ordinal analysis of bar recursion of type zero
JO  - Compositio Mathematica
PY  - 1980
SP  - 105
EP  - 119
VL  - 42
IS  - 1
PB  - Sijthoff et Noordhoff International Publishers
UR  - http://www.numdam.org/item/CM_1980__42_1_105_0/
LA  - en
ID  - CM_1980__42_1_105_0
ER  - 
%0 Journal Article
%A Howard, W. A.
%T Ordinal analysis of bar recursion of type zero
%J Compositio Mathematica
%D 1980
%P 105-119
%V 42
%N 1
%I Sijthoff et Noordhoff International Publishers
%U http://www.numdam.org/item/CM_1980__42_1_105_0/
%G en
%F 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 | Zbl

[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 | Zbl

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

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

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

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

[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 | Zbl