Friday, August 24, 2018 1:30 PM EDT
Ellen Arteca, Master’s candidate
David R. Cheriton School of Computer Science
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.
Location
DC - William G. Davis Computer Research Centre
2310
200 University Avenue West
Waterloo, ON N2L 3G1
Canada
200 University Avenue West
Waterloo, ON N2L 3G1
Canada