In this talk we will introduce System I, an intersection type system, and the basics of type inference within it. System I is interesting because has it principal typings. Principal typings allow for, among other things, efficient incremental analysis and separate compilation. Principality of System I is made possible by introducing the notion of expansions and expansion variables. We will conclude with a discussion of work in progress on different proposals for extending System I with sum types.
Host: Frank Pfenning
Appointments: Jennifer Landefeld
Principles of Programming Seminars