Document Open Access Logo

Trust, but Verify: Two-Phase Typing for Dynamic Languages

Authors Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.52.pdf
  • Filesize: 0.66 MB
  • 24 pages

Document Identifiers

Author Details

Panagiotis Vekris
Benjamin Cosman
Ranjit Jhala

Cite AsGet BibTex

Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. Trust, but Verify: Two-Phase Typing for Dynamic Languages. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 52-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.ECOOP.2015.52

Abstract

A key challenge when statically typing so-called dynamic languages is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave according to the types of its arguments. Thus, to establish basic types, the analysis must reason precisely about values, but in the presence of higher-order functions and polymorphism, this reasoning itself can require basic types. In this paper we address this chicken-and-egg problem by introducing the framework of two-phased typing. The first "trust" phase performs classical, i.e. flow-, path- and value-insensitive type checking to assign basic types to various program expressions. When the check inevitably runs into "errors" due to value-insensitivity, it wraps problematic expressions with DEAD-casts, which explicate the trust obligations that must be discharged by the second phase. The second phase uses refinement typing, a flow- and path-sensitive analysis, that decorates the first phase's types with logical predicates to track value relationships and thereby verify the casts and establish other correctness properties for dynamically typed languages.
Keywords
  • Dynamic Languages
  • Type Systems
  • Refinement Types
  • Intersection Types
  • Overloading

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Christopher Anderson, Paola Giannini, and Sophia Drossopoulou. Towards Type Inference for Javascript. In Proc. of the 19th European Conf. on Object-Oriented Programming, 2005. Google Scholar
  2. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement Types for Secure Implementations. ACM Trans. Program. Lang. Syst., 33(2), February 2011. Google Scholar
  3. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. Semantic Subtyping with an SMT Solver. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, 2010. Google Scholar
  4. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications. Int. J. Softw. Tools Technol. Transf., 7(3), June 2005. Google Scholar
  5. Robert Cartwright and Mike Fagan. Soft Typing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 1991. Google Scholar
  6. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A Calculus for Overloaded Functions with Subtyping. In Proc. of the 1992 ACM Conf. on LISP and Functional Programming, 1992. Google Scholar
  7. Ravi Chugh, Patrick M. Rondon, and Ranjit Jhala. Nested Refinements: A Logic for Duck Typing. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012. Google Scholar
  8. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, 1977. Google Scholar
  9. Joshua Dunfield. Untangling Typechecking of Intersections and Unions. In Proc. of the 5th Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July 2010, 2010. Google Scholar
  10. Joshua Dunfield. Elaborating Intersection and Union Types. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, 2012. Google Scholar
  11. Flow: A Static Type Checker for JavaScript. URL: http://flowtype.org.
  12. Asger Feldthaus and Anders Møller. Checking Correctness of TypeScript Interfaces for JavaScript Libraries. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Language and Applications, 2014. Google Scholar
  13. Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino. Annotation Inference for Modular Checkers. Inf. Process. Lett., 77(2-4), February 2001. Google Scholar
  14. Robert W. Floyd. Assigning Meanings to Programs. Proceedings of Symposium on Applied Mathematics, 19, 1967. Google Scholar
  15. Michael Furr, Jong-hoon (David) An, Jeffrey S. Foster, and Michael Hicks. Static Type Inference for Ruby. In Proc. of the 2009 ACM Symp. on Applied Computing, 2009. Google Scholar
  16. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. Typing Local Control and State Using Flow Analysis. In Proc. of the 20th European Conf. on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software, 2011. Google Scholar
  17. Fritz Henglein and Jakob Rehof. Safe Polymorphic Type Inference for a Dynamically Typed Language: Translating Scheme to ML. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, 1995. Google Scholar
  18. Kenneth Knowles and Cormac Flanagan. Hybrid Type Checking. ACM Trans. Program. Lang. Syst., 32(2), February 2010. Google Scholar
  19. Benjamin S. Lerner, Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. TeJaS: Retrofitting Type Systems for JavaScript. In Proc. of the 9th Symp. on Dynamic Languages, 2013. Google Scholar
  20. Phúc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. Soft Contract Verification. In Proc. of the 19th ACM SIGPLAN International Conf. on Functional Programming, 2014. Google Scholar
  21. Benjamin C. Pierce. Programming With Intersection Types, Union Types, and Polymorphism. PhD thesis, Carnegie Mellon University, 1991. Google Scholar
  22. John C. Reynolds. ALGOL-like Languages, Volume 1. In Peter W. O'Hearn and Robert D. Tennent, editors, Algol-like Languages, chapter Design of the Programming Language FORSYTHE. Birkhauser Boston Inc., Cambridge, MA, USA, 1997. Google Scholar
  23. Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid Types. In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2008. Google Scholar
  24. Jeremy Siek and Walid Taha. Gradual Typing for Objects. In Proce. of the 21st European Conf. on Object-Oriented Programming, 2007. Google Scholar
  25. The Satisfiability Modulo Theories Library. URL: http://smt-lib.org.
  26. Peter Thiemann. Towards a Type System for Analyzing Javascript Programs. In Proc. of the 14th European Conf. on Programming Languages and Systems, 2005. Google Scholar
  27. Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In Proc. of the 35th Annual ACM SIGPLAN-SIGACT Symp.on Principles of Programming Languages, 2008. Google Scholar
  28. Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. In Proc. of the 15th ACM SIGPLAN International Conf. on Functional Programming, 2010. Google Scholar
  29. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement Types for Haskell. In Proc. of the 19th ACM SIGPLAN International Conf. on Functional Programming, 2014. Google Scholar
  30. Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. Trust but Verify: Two-Phase Typing for Dynamic Languages - Extended. URL: http://arxiv.org/abs/1504.08039.
  31. Hongwei Xi and Frank Pfenning. Dependent Types in Practical Programming. In Proc. of the 26th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 1999. Google Scholar
  32. Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, and Michael D. Ernst. Object and Reference Immutability Using Java Generics. In Proc. of the the 6th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on The Foundations of Software Engineering, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact