An Abstract Interpretation Framework for Type and Effect Systems

Issue title: Theoretical Computer Science

Article type: Research Article

Authors: Galletta, Letterio

Affiliations: Dipartimento di Informatica, Universita di Pisa, galletta@di.unipi.it

Note: [] Address for correspondence: Dipartimento di Informatica, Bruno Largo Pontecorvo 3, 56127, Pisa, Italia

Abstract: 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.

DOI: 10.3233/FI-2014-1106

Journal: Fundamenta Informaticae, vol. 134, no. 3-4, pp. 355-393, 2014