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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.