Voir la notice de l'article provenant de la source Numdam
@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://geodesic.mathdoc.fr/item/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://geodesic.mathdoc.fr/item/CM_1968__20__107_0/