In Types as Abstract Interpretations, Cousot seems to propose a method to derive various type systems by succesive abstract interpretation of the denotational semantics of an untyped lambda-calculus. There is a key step missing from the paper. It is claimed that:
For clarity of the presentation, the design of the Church/-Curry monotype semantics $T^C ⟦\cdot⟧$ by abstract interpretation of the collecting semantics $C ⟦\cdot⟧$ is postponed to Section 7. Anyway the result is well-known:
However, in section 7 he rather addresses the polytype to monotype abstraction. In summary, what I'm looking for is an explanation on how one derives the type system of Church/Curry monotype semantics (which to me looks like the STLC + recursion + some integer constructs) by abstract interpretation of the semantics.