Types as abstract interpretations
inspired by a paper of Cousot (POPL ‘97), which
- derives several type abstract semantics from a collecting semantics for eager untyped lambda calculus
- including à la Church/Curry polytypes (with polymorphic recursion and abstraction)
- discusses their relation to “more traditional” rule based presentations
most of the abstract semantics are not “effective”
- infinite sets of monotypes in the abstract domain
- non-effective semantics for lambda abstraction