no. 1
Infinite terms and a system of natural deduction
Compositio Mathematica, Tome 24 (1972) no. 1, pp. 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},
     pages = {93--103},
     publisher = {Wolters-Noordhoff Publishing},
     volume = {24},
     number = {1},
     year = {1972},
     mrnumber = {300860},
     zbl = {0237.02006},
     language = {en},
     url = {http://www.numdam.org/item/CM_1972__24_1_93_0/}
}
TY  - JOUR
AU  - Martin-Löf, Per
TI  - Infinite terms and a system of natural deduction
JO  - Compositio Mathematica
PY  - 1972
SP  - 93
EP  - 103
VL  - 24
IS  - 1
PB  - Wolters-Noordhoff Publishing
UR  - http://www.numdam.org/item/CM_1972__24_1_93_0/
LA  - en
ID  - CM_1972__24_1_93_0
ER  - 
%0 Journal Article
%A Martin-Löf, Per
%T Infinite terms and a system of natural deduction
%J Compositio Mathematica
%D 1972
%P 93-103
%V 24
%N 1
%I Wolters-Noordhoff Publishing
%U http://www.numdam.org/item/CM_1972__24_1_93_0/
%G en
%F CM_1972__24_1_93_0
Martin-Löf, Per. Infinite terms and a system of natural deduction. Compositio Mathematica, Tome 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 | Zbl

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

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

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

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

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

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