Show simple item record

dc.contributor.authorArteca, Ellen 18:51:06 (GMT) 18:51:06 (GMT)
dc.description.abstractAs 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 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. 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. 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.en
dc.publisherUniversity of Waterlooen
dc.subjectFormal semanticsen
dc.subjectGradual typingen
dc.subjectSoundness proofen
dc.subjectProgramming languagesen
dc.titleFormal Semantics and Mechanized Soundness Proof for Fast Gradually Typed JavaScripten
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorRichards, Gregor
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages