A Formalization of Typed Lua
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 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00
Session 2, Formalization, Semantics, and Static AnalysisDLS at Grand Station 3
|A Formalization of Typed Lua|
Andre Murbach Maidl PUCPR, Fabio Mascarenhas UFRJ, Roberto Ierusalimschy PUC-RioMedia Attached
|Gradual Certified Programming in Coq|
Éric Tanter University of Chile, Chile, Nicolas Tabareau Inria
|Message Safety in Dart|
Erik Ernst , Mathias Schwarz Uber Aarhus, Fabio Strocco Aarhus University, Denmark, Anders Møller Aarhus University
|Control-Flow Analysis of Dynamic Languages via Pointer Analysis|
Steven Lyde , Matthew Might University of Utah, USA, William E. Byrd