Gradual Enforcement of Program Invariants
January 16, 2018 at 12:00pm (lunch talk)
Static and dynamic techniques have long been used to check and enforce properties of program executions. They are often seen as diametrically opposed, as exemplified by the long-running kerfuffle over the merits and deficits of static versus dynamic type checking.
Recently, PL researchers and designers have sought to bridge the divide between these approaches to program checking and analysis. In particular, Gradual Typing sets out to seamlessly combine static and dynamic checking of how closely programs adhere to standard typing disciplines from the literature. In this context, static and dynamic checking and enforcement are treated as complementary rather than conflicting.
In this talk I will discuss the theory and practice of gradual typing. Both have undergone significant development in the last few years. These advances in language design change not only how dynamic and static checking can work together, but also change how we think about each individually.
Ronald Garcia is an associate professor of Computer Science at the University of British Columbia. His research investigates how fundamental concepts in the theory, implementation, and practice of programming languages can improve the software development process. His research has focused on static and dynamic type-based reasoning, metaprogramming, and generic programming.
Prior to his appointment at UBC, he was a Computing Innovation Fellow at Carnegie Mellon University and Postdoctoral Fellow at Rice University. He received a PhD in Computer Science from Indiana University, and an MSc and BSc in Electrical Engineering from the University of Notre Dame.