Efficient Runtimes for Gradual Typing

454 pagesSupplemental file(s) description: Mechanized Proofs for Chapter 3.This dissertation concerns the design and implementation of programming languages featuring gradual typing - which is the idea that some parts of a program may be type-checked dynamically while others are type-checked statically. This lets programmers trade off between the costs and benefits of using static type-checking for each individual part of their program as needed, and even eventually change their decisions about those trade-offs. Designing gradually typed languages has its own trade-offs: existing gradually typed languages had to essentially decide between being efficient versus behaving in expected and safe ways. Since many of those languages were just gradually typed variants of existing languages, those trade-offs were largely forced by the original language design. Here, we look at the design questions around gradual typing in an unconstrained scenario - what if we design a new language featuring gradual typing from the ground up? In particular, we explore these questions for nominal object-oriented programming languages. Designing a new language from the ground up lets us *co-design* the features of the language and its implementation. Accordingly, in this dissertation, we tackle a variety of design questions of particular importance to gradual typing, such as decidable subtyping, as well as questions of implementation, most importantly efficient casting techniques, which we evaluate using benchmarks from the literature on efficiency in gradual typing. The results presented here show that when gradual typing is co-designed with the rest of the type system and with an eye towards efficiency, it is possible to obtain both the desired formal properties proposed so far for gradual type systems and very low overheads due to gradual typing. This points the way towards a new generation of programming languages that can be used to seamlessly transition between personal scripting or rapid prototyping and large-scale software engineering