@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://archive.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://archive.numdam.org/item/CM_1972__24_1_93_0/
Combinatory logic, vol. I (North-Holland, Amsterdam) 1958. | MR | Zbl
ANDUntersuchungen über das logische Schliessen, Math. Z. 39 (1934) 176-210, 405-431. | JFM | Zbl
The formulae-as-types notion of construction, privately circulated notes, 1969.
Natural deduction (Almqvist & Wiksell, Stockholm) 1965. | MR | Zbl
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
Continuous increasing functions of finite and transfinite ordinals, Trans. Amer. Math. Soc. 9 (1908) 280-292). | JFM | MR