Master’s Thesis Presentation • Programming Languages — Formal Semantics and Mechanized Soundness Proof for Fast Gradually Typed JavaScript

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 lead 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. In gradual typing, there is also a guarantee that any runtime type errors will be caught when they cross the boundary from typed to untyped code – type checks are inserted at runtime to ensure this. These runtime checks have the downside of adding significant overhead to the execution time, so much so that a recent paper [19] considered it potentially untenable.

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.