License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2016.1
URN: urn:nbn:de:0030-drops-60952
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6095/
Go to the corresponding LIPIcs Volume Portal

Andreasen, Esben ; Gordon, Colin S. ; Chandra, Satish ; Sridharan, Manu ; Tip, Frank ; Sen, Koushik

Trace Typing: An Approach for Evaluating Retrofitted Type Systems

pdf-format:
LIPIcs-ECOOP-2016-1.pdf (0.8 MB)

Abstract

Recent years have seen growing interest in the retrofitting of
type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking.

We present trace typing: a framework for automatically and
quantitatively evaluating variations of a retrofitted type system
on large code bases. The trace typing approach involves gathering
traces of program executions, inferring types for instances of
variables and expressions occurring in a trace, and merging types
according to merge strategies that reflect specific (combinations
of) choices in the source-level type system design space.

We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.

BibTeX - Entry

@InProceedings{andreasen_et_al:LIPIcs:2016:6095,
  author =	{Esben Andreasen and Colin S. Gordon and Satish Chandra and Manu Sridharan and Frank Tip and Koushik Sen},
  title =	{{Trace Typing: An Approach for Evaluating Retrofitted Type Systems}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{1:1--1:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Shriram Krishnamurthi and Benjamin S. Lerner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6095},
  URN =		{urn:nbn:de:0030-drops-60952},
  doi =		{10.4230/LIPIcs.ECOOP.2016.1},
  annote =	{Keywords: Retrofitted type systems, Type system design, trace typing}
}

Keywords: Retrofitted type systems, Type system design, trace typing
Collection: 30th European Conference on Object-Oriented Programming (ECOOP 2016)
Issue Date: 2016
Date of publication: 18.07.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI