William Stirton

While this may be of interest mainly to people who have some interest in the polymorphically typed lambda calculus, the only knowledge I assume is, roughly, that you know what a polymorphic type is, plus some facts about the simply typed lambda calculus and the formulae-types correspondence (the Curry-Howard isomorphism). I do not assume you know what combinatory logic is. Model theory will not come into it. So if, like me, you find the model theory of the lambda calculus a bit scary, you need have no fear on that account. 

The main new result I have to announce concerns a subsystem of polymorphically typed combinatory logic which is equivalent to Goedel's T. I have an answer to the question: how many reduction steps are needed to normalize a term within this subsystem? The answer is not surprising but I think it is at least new.