Formal Semantics and Mechanized Soundness Proof for Fast Gradually Typed JavaScript

Formal semantics;Gradual typing;JavaScript;Soundness proof;Mechanization;Programming languages

Arteca, Ellenaffiliation1:Faculty of Mathematics ; advisor:Richards, Gregor ; Richards, Gregor ;

University of Waterloo

关键词: Gradual typing;    Master Thesis;    JavaScript;    Mechanization;    Soundness proof;    Formal semantics;    Programming languages;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/13697/1/Arteca_Ellen.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

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 gradualtyping, a typing paradigm which is a compromise betweenstaticanddynamictyping.Ingradualtyping,programmerscanspecifytype 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. Inthisthesis,weconsidertheworkwepresentedin[15],forafastgradually 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.