Spring Semester

Integrating Static and Dynamic Type Systems

Lecturer: Professor Philip Wadler (University of Edinburgh, UK).

About the lecturer | Course Summary | Slides: 1 2 3 4 | Assignment

About the lecturer: Philip Wadler likes to introduce theory into practice, and practice into theory. An example of theory into practice: GJ, the basis for Java with generics, derives from quantifiers in second-order logic. An example of practice into theory: Featherweight Java specifies the core of Java in less than one page of rules. He is a principal designer of the Haskell programming language, contributing to its two main innovations, type classes and monads.

Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past holder of a Royal Society-Wolfson Research Merit Fellowship, and currently serves as Chair of ACM SIGPLAN. Previously, he worked or studied at Avaya Labs, Bell Labs, Glasgow, Chalmers, Oxford, CMU, Xerox Parc, and Stanford, and visited as a guest professor in Paris, Sydney, and Copenhagen. He appears at position 269 of Citeseer's list of most-cited authors in computer science and is a winner of the POPL Most Influential Paper Award. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O'Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.

Course summary: Both Meijer and Bracha argue in favor of mixing dynamic and static typing, and such mixing is now supported in Microsoft's .NET framework. Much recent work has focused on integrating dynamic and static typing using the contracts of Findler and Felleisen, including the gradual types of Siek and Taha, the hybrid types of Flanagan, and the manifest contracts of Greenberg, Pierce, and Weirich. This course will focus on the blame calculus, which unifies the above approaches, permitting one to integrate several strengths of type system: dynamically typed languages, Hindley-Milner typed languages, and refinement types. We will cover the basics of the blame calculus, its extension to support parametric polymorphism, and implementation techniques based on threesomes.

Slides: 1 2 3 4

Bibliography

Assignment
Please send the solution (pdf) to professor Wadler (wadler AT inf DOT ed DOT ac DOT uk) by 23 January, 2012.