Tait, W. W., Nested Recursion Tait, W. W., Infinitely Long Terms of Transfinite Type (1963) Takahashi, Moto-o, A Proof of Cut-Elimination Theorem in Simple Type-Theory Takahashi, Moto-o, Ackermann's Model and Recursive Predicates (1968) Takahashi, Moto-o, On Incomparable Cardinals (1968) Takahashi, Moto-o, Recursive Functions of Ordinal Numbers and Levy's Hierarchy (1968) Takahashi, Moto-o, Simple Type Theory of Gentzen Style with the Inference of Extensionality (1968) Takahashi, Moto-o, An Induction Principle in Set Theory I (1969) Takahashi, Moto-o, A System of Simple Type Theory of Gentzen Style with Inference on Extensionality, and the Cut-Elimination in it (1970) Takahashi, Moto-o, Continuous $\lambda - \varepsilon$ Logics (1970)