Gradual typing is an approach for designing programming languages that integrate static and dynamic type checking. Gradual typing gives the programmer control over which regions of a program are statically checked and which regions are dynamically checked. Over the last decade, there has been renewed interest in such an integration partly due to the rise in popularity of dynamic languages. They have been used to create large programs, which exposed the need for the early error detection and modularity provided by static type checking. Gradual typing provides a practical migration path for dynamically typed programs to become more statically typed. This lecture will give a comprehensive review of the state of the art in gradual typing. It will describe a) the major challenges in the design and implementation of gradually typed languages, b) the research that has addressed many of of these challenges, and c) the open problems that need to be solved. The challenges facing gradual typing include both theoretical questions and system design problems. On the theoretical side, there are challenges like characterizing what gradual typing is, what type soundness should mean, and whether relational parametricity can be preserved. On the system design side, there are challenges such as creating language runtimes that implement gradual typing in a time and space-efficient manner.

Jeremy Siek is an Associate Professor at Indiana University Bloomington. Jeremy’s areas of research include programming language design, type systems, mechanized theorem proving using proof assistants, and optimizing compilers. Jeremy’s Ph.D. thesis explored foundations for constrained templates, aka the “concepts” proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc’d at Rice University with Walid Taha with whom he developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on a gradually-typed version of Pytho. In 2009 Jeremy received the NSF CAREER award to fund his project: “Bridging the Gap Between Prototyping and Production”. In 2010 and again in 2015, Jeremy was awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance.