1 Search Results for "Vekris, Panagiotis"

Document
DOI: 10.4230/LIPIcs.ECOOP.2015.52
Trust, but Verify: Two-Phase Typing for Dynamic Languages

Authors: Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{vekris_et_al:LIPIcs.ECOOP.2015.52,
  author =	{Vekris, Panagiotis and Cosman, Benjamin and Jhala, Ranjit},
  title =	{{Trust, but Verify: Two-Phase Typing for Dynamic Languages}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{52--75},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.52},
  URN =		{urn:nbn:de:0030-drops-52173},
  doi =		{10.4230/LIPIcs.ECOOP.2015.52},
  annote =	{Keywords: Dynamic Languages, Type Systems, Refinement Types, Intersection Types, Overloading}
}
  • Refine by Author
  • 1 Cosman, Benjamin
  • 1 Jhala, Ranjit
  • 1 Vekris, Panagiotis

  • Refine by Classification

  • Refine by Keyword
  • 1 Dynamic Languages
  • 1 Intersection Types
  • 1 Overloading
  • 1 Refinement Types
  • 1 Type Systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

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