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.

Dataflow analysis is a powerful tool used for program optimization, static analysis, and editor services for many programming languages. Spoofax, a language workbench, contains a domain-specific language called FlowSpec for the definition of control-flow and dataflow semantics that language developers can use to implement dataflow analyses for their language. FlowSpec however cannot be used to efficiently optimize programs. Other solutions are not suitable for language developers, or lack the ergonomics of a domain-specific language. In this thesis we present Flock: an incremental implementation of FlowSpec. We analyze the performance of Flock and show that it is efficient enough for use in optimization pipelines. Flock gives language developers the tools to succinctly write dataflow analyses for a wide variety of applications.