In Types as Abstract Interpretation, Patrick Cousot sketched how different type systems could be constructed from the collecting semantics of a language. However, the notation of the paper is very old and I'm not able to reconstruct it.

Does anybody see what would be an abstract interpretation corresponding to the simply typed lambda calculus as described in for instance figure 9-1 of the TAPL book?

  • 1
    $\begingroup$ I think this is too broad to be answered here. You are essentially asking to explain in more detail the whole paper. (Further, to be honest, I can't believe Cousot can't understand his own paper as you seem to claim.) Maybe you should try to focus the question to a specific point. $\endgroup$
    – chi
    May 19 '20 at 8:06
  • $\begingroup$ @chi the paper addresses more topics than this. there is a distinction between monotype and polytype semantics as well as seen different abstract interpretations of different type systems. i will add the details of the particular case i'm asking about (which is not the whole paper) $\endgroup$
    – Rodrigo
    May 19 '20 at 9:08

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.