An Abstract Interpretation Framework for Type and Effect Systems

Type and effect systems significantly extend type systems and allow one to express general semantic properties and to statically reason about programs execution. They have been widely exploited to specify static analyses, for example to track computational side effects, resource usage and communication in concurrent languages. In this paper we adopt abstract interpretation techniques to express type and effect systems as abstract semantics. We extend the Cousot's methodology by introducing an abstract domain which (i) is able to express types with annotations, (ii) is reusable in different analyses with few modifications and (iii) is easily implementable. To test our approach we reconstruct two analyses for which the type and effect systems approach were successful.