Formal Semantics and Mechanized Soundness Proof for Fast Gradually Typed JavaScript

Abstract

As dynamic scripting languages are increasingly used in industry in large-scale projects, a need has arisen for more some of the convenient features of statically typed languages. This led to the development of gradual typing, a typing paradigm which is a compromise between static and dynamic typing. In gradual typing, programmers can specify type annotations if and when they choose to; then, at compile time, the statically typed sections of code are type checked. Gradual typing also guarantees that any runtime type errors will be caught when they cross the boundary from typed to untyped code, inserting type checks at runtime to ensure this. These runtime checks have the downside of adding significant overhead to the execution time, to the point where Takikawa et al. suggest it is practically untenable, in their paper [19].

Recent work has been done to develop faster implementations of sound gradually typed systems. In this thesis, we consider the work we presented in [15], for a fast gradually typed implementation of JavaScript, a popular dynamic scripting language. This thesis presents the formal semantics of this type system, and provides a mechanized soundness proof using the Coq proof assistant.