Provably Sound Typechecking of JavaScript
M.D. Bijman (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S. Keidel – Mentor
Sebastian Erdweg – Graduation committee member
R.J. Krebbers – Graduation committee member
C. Dörr – Graduation committee member
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Since its inception in 1995, JavaScript usage has grown far beyond its initial domain of interactive websites. As the size of applications developed in the language grows, so does the desire for static analysis such as typechecking to provide safety and reliability. Many developments have been made in recent years on increasing the precision of analysis of JavaScript. This work introduces a concrete and a type interpreter for LambdaJS implemented within the Sturdy framework. The goal of this work is to evaluate the feasibility of implementing a shared interpreter using the Sturdy framework, evaluate the correctness of the concrete interpreter, and evaluate the feasibility of proving the typechecker sound. The resulting interpreters are tested experimentally with two test suites. The experimental evaluation gives confidence in the correctness of the concrete and abstract interpreter. A small part of the abstract interpreter is proven sound to evaluate the difficultyofcreatingacompletesoundnessproof.Thesuccessful implementation of the interpreters shows that implementing a shared arrow-based interpreter within the Sturdy framework is feasible for languages with complex semantics, that the utilities available reduce the effort required to do so, and that proving the abstract interpreter sound is simplified by using the library.