An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language

Letterio Galletta
(Dipartimento di Informatica, Università di Pisa)
Giorgio Levi
(Dipartimento di Informatica, Università di Pisa)

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 analyses, 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.

In Laura Kovacs, Rosario Pugliese and Francesco Tiezzi: Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011), Reykjavik, Iceland, 9th June 2011, Electronic Proceedings in Theoretical Computer Science 61, pp. 81–95.
Published: 10th August 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: