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.SNAPL.2015.274
URN: urn:nbn:de:0030-drops-50312
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5031/
Go to the corresponding LIPIcs Volume Portal

Siek, Jeremy G. ; Vitousek, Michael M. ; Cimini, Matteo ; Boyland, John Tang

Refined Criteria for Gradual Typing

pdf-format:
21.pdf (0.6 MB)

Abstract

Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations. We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.

BibTeX - Entry

@InProceedings{siek_et_al:LIPIcs:2015:5031,
  author =	{Jeremy G. Siek and Michael M. Vitousek and Matteo Cimini and John Tang Boyland},
  title =	{{Refined Criteria for Gradual Typing}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{274--293},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Thomas Ball and Rastislav Bodik and Shriram Krishnamurthi and Benjamin S. Lerner and Greg Morrisett},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5031},
  URN =		{urn:nbn:de:0030-drops-50312},
  doi =		{10.4230/LIPIcs.SNAPL.2015.274},
  annote =	{Keywords: gradual typing, type systems, semantics, dynamic languages}
}

Keywords: gradual typing, type systems, semantics, dynamic languages
Collection: 1st Summit on Advances in Programming Languages (SNAPL 2015)
Issue Date: 2015
Date of publication: 30.04.2015

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