Programmers often migrate from a dynamically typed to a statically typed language when their simple scripts evolve into complex programs. Optional type systems are one way of having both static and dynamic typing in the same language, while keeping its dynamically typed semantics. This makes evolving a program from dynamic to static typing a matter of describing the implied types that it is using and adding annotations to make those types explicit. Designing an optional type system for an existing dynamically typed language is challenging, as its types should feel natural to programmers that are already familiar with this language.

In this work, we give a formal description of Typed Lua, an optional type system for Lua, with a focus on two of its novel type system features: incremental evolution of imperative record and object types that is both lightweight and type-safe, and the combination of flow typing, functions that return multiple values, and multiple assignment. While our type system is tailored to the features and idioms of Lua, its features can be adapted to other imperative scripting languages.

Tue 27 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:00
Session 2, Formalization, Semantics, and Static AnalysisDLS at Grand Station 3
10:30
22m
Talk
A Formalization of Typed Lua
DLS
Media Attached
10:52
22m
Talk
Gradual Certified Programming in Coq
DLS
Éric Tanter University of Chile, Chile, Nicolas Tabareau Inria
11:15
22m
Talk
Message Safety in Dart
DLS
Erik Ernst , Mathias Schwarz Uber Aarhus, Fabio Strocco Aarhus University, Denmark, Anders Møller Aarhus University
11:37
22m
Talk
Control-Flow Analysis of Dynamic Languages via Pointer Analysis
DLS
Steven Lyde , Matthew Might University of Utah, USA, William E. Byrd