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?