This work is licensed under the Creative Commons Attribution-Noncommercial License. An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language

Types-and-effects are type systems, which allow one to express general semantic properties and to statically reason about program’s execution. They have been widely exploited to specify static ana-lyses, for example to track computational side effects, exceptions and communications in concurrent programs. In this paper we adopt abstract interpretation techniques to reconstruct (following the Cousot’s methodology) a types-and-effects system developed to handle security problems of a multi-tier web language. Our reconstruction allows us to show that this types-and-effects system is not sound with respect to the semantics of the language. In addition, we correct the soundness issues in the analysis and systematically construct a correct analyser.