Infinite terms and a system of natural deduction
Compositio Mathematica, Volume 24 (1972) no. 1, p. 93-103 
@article{CM_1972__24_1_93_0,
     author = {Martin-L\"of, Per},
     title = {Infinite terms and a system of natural deduction},
     journal = {Compositio Mathematica},
     publisher = {Wolters-Noordhoff Publishing},
     volume = {24},
     number = {1},
     year = {1972},
     pages = {93-103},
     zbl = {0237.02006},
     mrnumber = {300860},
     language = {en},
     url = {http://www.numdam.org/item/CM_1972__24_1_93_0}
}

Martin-Löf, Per. Infinite terms and a system of natural deduction. Compositio Mathematica, Volume 24 (1972) no. 1, pp. 93-103. http://www.numdam.org/item/CM_1972__24_1_93_0/

H.B. Curry AND R. Feys Combinatory logic, vol. I (North-Holland, Amsterdam) 1958. | MR 94298 | Zbl 0175.27601

G. Gentzen Untersuchungen über das logische Schliessen, Math. Z. 39 (1934) 176-210, 405-431. | JFM 60.0846.01 | Zbl 0010.14601

W.A. Howard The formulae-as-types notion of construction, privately circulated notes, 1969.

D. Prawitz Natural deduction (Almqvist & Wiksell, Stockholm) 1965. | MR 193005 | Zbl 0173.00205

W.W. Tait Infinitely long terms of transfinite type, Formal Systems and Recursive Functions, edited by J. N. Crossley and M. A. E. Dummet (North-Holland, Amsterdam), (1965) 176-185. | MR 195727 | Zbl 0154.00504

Normal derivability in classical logic, Lecture Notes in Mathematics (Springer-Verlag, Berlin), 72 (1968) 204-236. | Zbl 0206.00502

O. Veblen Continuous increasing functions of finite and transfinite ordinals, Trans. Amer. Math. Soc. 9 (1908) 280-292). | JFM 39.0102.01 | MR 1500814