Functional interpretation of bar induction by bar recursion
Compositio Mathematica, Tome 20 (1968), pp. 107-124. 
@article{CM_1968__20__107_0,
     author = {Howard, W. A.},
     title = {Functional interpretation of bar induction by bar recursion},
     journal = {Compositio Mathematica},
     pages = {107--124},
     publisher = {Wolters-Noordhoff Publishing},
     volume = {20},
     year = {1968},
     mrnumber = {230619},
     zbl = {0162.31503},
     language = {en},
     url = {http://www.numdam.org/item/CM_1968__20__107_0/}
}
TY  - JOUR
AU  - Howard, W. A.
TI  - Functional interpretation of bar induction by bar recursion
JO  - Compositio Mathematica
PY  - 1968
SP  - 107
EP  - 124
VL  - 20
PB  - Wolters-Noordhoff Publishing
UR  - http://www.numdam.org/item/CM_1968__20__107_0/
LA  - en
ID  - CM_1968__20__107_0
ER  - 
%0 Journal Article
%A Howard, W. A.
%T Functional interpretation of bar induction by bar recursion
%J Compositio Mathematica
%D 1968
%P 107-124
%V 20
%I Wolters-Noordhoff Publishing
%U http://www.numdam.org/item/CM_1968__20__107_0/
%G en
%F CM_1968__20__107_0
Howard, W. A. Functional interpretation of bar induction by bar recursion. Compositio Mathematica, Tome 20 (1968), pp. 107-124. http://www.numdam.org/item/CM_1968__20__107_0/

K. Gödel [1] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, 12 (1958), 280-287. | MR | Zbl

W.A. Howard and G. Kreisel [2] Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, Journal of Symbolic Logic 31 (1966), 325 - 358. | Zbl

S.C. Kleene and R.E. Vesley [3] Foundations of Intuitionistic Mathematics, North-Holland Publishing Co., Amsterdam, 1965. | MR | Zbl

G. Kreisel [4] Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics, North-Holland Publishing Co., Amsterdam, 1959, 101-128. | MR | Zbl

G. Kreisel [5] Proof by transfinite induction and definition by transfinite recursion, Journal of Symbolic Logic, 24 (1959), 322-323.

G. Kreisel [6] A survey of proof theory, Journal of Symbolic Logic, to appear. | MR | Zbl

C. Spector [7] Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Proceedings of the Symposia in Pure Mathematics, vol. 5, American Mathematical Society, Providence, 1962, 1- 27. | MR | Zbl