Thesis (Ph.D.) - Indiana University, School of Informatics, Computing, and Engineering, 2019Gradual typing integrates static and dynamic typing with the guarantee that statically typed regions of a program will never have their types violated even if they interact with dynamically typed regions. Traditionally, this guarantee has been achieved by using proxies to mediate when values flow between statically and dynamically typed code. However, languages such as Python cannot support these proxies, and so a different approach is needed to adapt gradual typing to Python. In my dissertation, I show that the guarded approach is a poor match for Python, but also that sound and efficient gradual typing for Python can be achieved with enforcement strategies that do not use proxies. I show two approaches for achieving soundness without proxies. The first, the monotonic approach for mutable references, uses runtime type information to ensure that data corresponds to all types at which it has been referenced, removing the need for proxies. However, the need to track this information is a serious challenge. Alternatively, lightweight transient checks may be inserted throughout the statically typed regions of the compiled program, which ensure that all values shallowly correspond to the static types they are expected to have. I implemented this strategy in a gradually typed version of Python, and found that the transient strategy is a good match with Python: transient checks can be straightforwardly implemented and are efficient. In order to improve the runtime performance of transient gradual typing, I developed a type-inference-based approach to erase transient checks when they can be statically shown to be redundant. I studied a number of benchmarks in Python with this implementation and found that the performance impact of transient gradual typing is minimal in most cases, especially when used in combination with PyPy, a JIT-based Python runtime.