  J.Y. Girard’s motivation for considering a type system with polymorphism was to extend Gödel’s Dialectica (Gödel 1958) interpretation to second-order arithmetic. He proved normalisation using the reducibility method, that had been introduced by Tait (1967) while analysing Gödel 1958. It is quite remarkable that the circularity inherent in impredicativity does not result in non-normalisable terms. (Girard’s argument was then used to show that cut-elimination terminates in Takeuti’s sequent calculus presented above.) A similar system was introduced independently by J. Reynolds (1974) while analysing the notion of polymorphism in computer science.