SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Mon 20 Oct 2014 11:30 - 12:00 at Salon G - Research Papers Chair(s): Marco Servetto

Abstract: This paper establishes a notion of message-safe programs as a natural intermediate point between dynamically typed and statically typed Dart programs. Unlike traditional static type checking, the type system in the Dart programming language is unsound by design. The rationale has been that this allows compile-time detection of likely errors and enables code completion in integrated development environments, without being restrictive on programmers. We show that, despite unsoundness, judicious use of type annotations can ensure useful properties of the runtime behavior of Dart programs. This supports evolution from a dynamically typed program to a strictly statically typed form. We present a formal model of Dart that elucidates how a core of the language and its standard type system works. This allows us to characterize message-safe programs and present a theorem stating that such programs will never cause ‘message not understood’ errors, which is generally not guaranteed for Dart programs that pass the standard type checker. The formal model has been expressed in Coq.

Mon 20 Oct

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Research PapersFOOL at Salon G
Chair(s): Marco Servetto Victoria University of Wellington
10:30
30m
Talk
Program Equivalence through Trace Equivalence
FOOL
Tim Wood Imperial College, Sophia Drossopoulou Imperial College London
File Attached
11:00
30m
Talk
The Problem of Structural Type Tests in a Gradual-Typed Language
FOOL
John Boyland University of Wisconsin, Milwaukee
File Attached
11:30
30m
Talk
Managing Gradual Typing with Message-Safety in Dart
FOOL
File Attached