# Types as abstract interpretations

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.

• Maybe of interests is this CST question. – Martin Berger Mar 20 at 10:45
• Your question elicits just a "yes/no" answer. You may want to rephrase it to clarify what it is you really want to know. – Stefan Mar 21 at 15:29
• @Stefan I have rephrased my question. Thanks for the advice – Rodrigo Mar 26 at 23:09