Ronald Garcia

What type of thing is a type?

Types and type systems come up all the time when we talk about, learn, and use programming languages. Programmers have many useful intuitions about types, including what they are, what they have to offer, and how to think about and exploit them. Meanwhile, language theorists wrestle with these intuitions and work to make them even more precise: what in the world is a type? What is a type system? How can (and should) we formally reason about them?

In this talk, Ronald will unpack types and type systems from the perspectives of programming languages theorists, rather than practitioners. By spending quality time with some classic literature, we will see that formal theories about types and type systems have shifted back and forth and back again over time, depending on the challenges facing individual theorists, their conceptual stances, and the increasing sophistication and scope of types as part of language designs.

References

• Types Are Not Sets by J.H. Morris
• A Theory of Type Polymorphism in Programming by R. Milner
• Types, Abstraction, and Parametric Polymorphism by J.C. Reynolds
• Co-induction in Relational Semantics by R. Milner and M. Tofte
• Typing First-class Continuations in ML by B.F. Duba, R. Harper, and D. MacQueen
• A Syntactic Approach to Type Soundness by A.K. Wright and M. Felleisen
• Semantics of Types for Mutable State by A.J. Ahmed

Biography

Ronald Garcia is an associate professor in the Computer Science Department at University of British Columbia. His research investigates how fundamental concepts in the theory, implementation, and practice of programming languages can improve software development. His recent research has focused on program generation and metaprogramming, static and dynamic type systems, and generic programming abstractions.