An Abstract Interpretation Framework for Type and Effect Systems

• Autorzy: Galletta, L.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

semantics; programming languages; software frameworks; computer programming; systems theory

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 134, nr 3/4
• Strony: 355--393
• Opis fizyczny: Bibliogr. 40 poz.

Twórcy

autor

Galletta, L.

• Dipartimento di Informatica, Universita di Pisa,

Bibliografia

• [1] Baader, F., Siekmann, J. H.: Unification theory, in: Handbook of Logic in Artificial Intelligence and Logic Programming (2) (D. M. Gabbay, C. J. Hogger, J. A. Robinson, J. H. Siekmann, Eds.), Oxford University Press, 1994, ISBN 0-19-853746-8, 41–126.
• [2] Baltopoulos, I. G., Gordon, A. D.: Secure compilation of a multi-tier web language, Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009 (A. Kennedy, A. Ahmed, Eds.), 2009.
• [3] Bartoletti, M., Degano, P., Ferrari, G.-L., Zunino, R.: Local policies for resource usage analysis, ACM Trans. Program. Lang. Syst., 31(6), August 2009, 23:1–23:43, ISSN 0164-0925.
• [4] Cooper, E., Lindley, S., Wadler, P., Yallop, J.: Links: Web Programming Without Tiers, in: Formal Methods for Components and Objects (F. de Boer, M. Bonsangue, S. Graf,W.-P. de Roever, Eds.), vol. 4709 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2007, 266–296.
• [5] Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation, Computer Languages, Systems & Structures, 37(1), 2011, 24–42.
• [6] Cousot, P.: Types as Abstract Interpretations, invited paper, Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (P. Lee, F. Henglein, N. D. Jones, Eds.), ACM Press, New York, NY, Paris, France, January 1997.
• [7] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (R. M. Graham, M. A. Harrison, R. Sethi, Eds.), ACM Press, New York, NY, Los Angeles, California, 1977.
• [8] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks, Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (A. V. Aho, S. N. Zilles, B. K. Rosen, Eds.), ACM Press, New York, NY, San Antonio, Texas, 1979.
• [9] Cousot, P., Cousot, R.: Abstract Interpretation and Application to Logic Programs, Journal of Logic Programming, 13(2–3), 1992, 103–179.
• [10] Cousot, P., Cousot, R.: Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation, Proceedings of the Seventh ACM Conference on Functional Programming Languages and Computer Architecture, ACM Press, New York, NY, La Jolla, California, 25–28 June 1995.
• [11] Damas, L., Milner, R.: Principal type-schemes for functional programs, POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (R. A. DeMillo, Ed.), ACM, New York, NY, USA, 1982, ISBN 0-89791-065-6.
• [12] Davey, B. A., Priestley, H.: Introduction to Lattices and order, 2nd edition edition, Cambridge University Press, 2002, ISBN 978-0-521-78451-1.
• [13] Degano, P., Ferrari, G.-L., Galletta, L., Mezzetti, G.: Types for coordinating secure behavioural variations, Proceedings of the 14th international conference on Coordination Models and Languages (M. Sirjani, Ed.), 7274, Springer-Verlag, Berlin, Heidelberg, 2012, ISBN 978-3-642-30828-4.
• [14] Galletta, L.: Una semantica astratta per l’inferenza dei tipi ed effetti in un linguaggio multi-tier, Master Thesis, Università di Pisa, 2010.
• [15] Galletta, L.: A Reconstruction of a Type and Effect System, ICTCS 2012, 2012.
• [16] Galletta, L., Levi, G.: An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language, Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems (L. Kovács, R. Pugliese, F. Tiezzi, Eds.), 61, 2011.
• [17] Gifford, D. K., Lucassen, J. M.: Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, LFP ’86, ACM, New York, NY, USA, 1986, ISBN 0-89791-200-4.
• [18] Gori, R., Levi, G.: An Experiment in Type Inference and Verification by Abstract Interpretation, VMCAI ’02: Revised Papers from the Third International Workshop on Verification, Model Checking, and Abstract Interpretation (A. Cortesi, Ed.), 2294, Springer-Verlag, London, UK, 2002, ISBN 3-540-43631-6.
• [19] Gori, R., Levi, G.: Properties of a Type Abstract Interpreter, in: Verification, Model Checking, and Abstract Interpretation (L. Zuck, P. Attie, A. Cortesi, S. Mukhopadhyay, Eds.), vol. 2575 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2003, ISBN 978-3-540-00348-9, 132–145.
• [20] Gunter, C. A., Scott, D. S.: Semantic Domains, vol. Handbook of Theoretical Computer Science, chapter 12, Elsevier Science, 1990, 634–674.
• [21] Hindley, R.: The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, 146, 1969, 29–60.
• [22] INRIA: The Caml Language, WWW publication.
• [23] Lassez, J.-L., Maher, M. J., Marriott, K.: Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1988, ISBN 0-934613-40-0.
• [24] Leroy, X., Pessaux, F.: Type-based analysis of uncaught exceptions, ACM Trans. Program. Lang. Syst., 22(2), March 2000, 340–377, ISSN 0164-0925.
• [25] Levi, G., Volpe, P.: Derivation of Proof Methods by Abstract Interpretation, in: Proceedings of the 10th International Symposium on Principles of Declarative Programming (J. L. Freire-Nistal, M. Falaschi, M. V. Ferro, Eds.), PLILP ’98/ALP ’98, Springer-Verlag, London, UK, UK, 1998, ISBN 3-540-65012-1, 102–117.
• [26] Martelli, A., Montanari, U.: An Efficient Unification Algorithm, ACM Trans. Program. Lang. Syst., 4(2), 1982, 258–282.
• [27] Meijer, E., Schulte,W., Bierman, G.: Programming with circles, triangles and rectangles, In XML Conference and Exposition, 2003.
• [28] Monsuez, B.: Polymorphic Typing by Abstract Interpretation, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science (R. K. Shyamasundar, Ed.), 652, Springer-Verlag, London, UK, 1992, ISBN 3-540-56287-7.
• [29] Monsuez, B.: Polymorphic types and widening operators, in: Static Analysis (P. Cousot, M. Falaschi, G. FilĂ© , A. Rauzy, Eds.), vol. 724 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1993, ISBN 978-3-540-57264-0, 267–281.
• [30] Monsuez, B.: Polymorphic typing for call-by-name semantics, in: Formal Methods in Programming and Their Applications (D. Bjørner, M. Broy, I. Pottosin, Eds.), vol. 735 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1993, ISBN 978-3-540-57316-6, 156–169.
• [31] Monsuez, B.: System F and abstract interpretation, in: Static Analysis (A. Mycroft, Ed.), vol. 983 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1995, ISBN 978-3-540-60360-3, 279–295.
• [32] Mycroft, A.: Polymorphic type schemes and recursive definitions, in: International Symposium on Programming (M. Paul, B. Robinet, Eds.), vol. 167 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1984, ISBN 978-3-540-12925-7, 217–228.
• [33] Nielson, F., Nielson, H.: Constraints for polymorphic behaviours of concurrent ML, in: Constraints in Computational Logics (J.-P. Jouannaud, Ed.), vol. 845 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 1994, 73–88.
• [34] Nielson, F., Nielson, H. R., Hankin, C.: Principles of Program Analysis, 1st ed. 1999. corr. 2nd printing, 1999 edition, Springer, 2005, ISBN 978-3-540-65410-0.
• [35] Pierce, B. C.: Types and programming languages, MIT Press, Cambridge, MA, USA, 2002, ISBN 0-262-16209-1.
• [36] Queinnec, C.: The influence of browsers on evaluators or, continuations to program web servers, SIGPLAN Not., 35, September 2000, 23–33, ISSN 0362-1340.
• [37] Reynolds, J.: Towards a theory of type structure, in: Programming Symposium (B. Robinet, Ed.), vol. 19 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1974, ISBN 978-3-540-06859-4, 408–425.
• [38] Schmidt, D.: Denotational Semantics: A Methodology for Language Development, William C Brown Pub, 1986, ISBN 0697068498.
• [39] Vouillon, J., Jouvelot, P.: Type and Effect Systems via Abstract Interpretation, 1995.
• [40] Winskel, G.: The Formal Semantics of Programming Languages, MIT Press, 1993, ISBN 978-0-262-73103-4.

Identyfikatory

DOI

10.3233/FI-2014-1106