Seminars & Colloquia
Appalachian State University
"Parametricity for Programmers"
Friday September 20, 2019 11:00 AM
Location: 3211, EB2 NCSU Centennial Campus
(Visitor parking instructions)
This talk is part of the Theory Seminar Series
enforcing invariants that guarantee strong properties of programs, programming languages, and programming language implementations supporting parametric polymorphic functions. A program is polymorphic if it can be applied to arguments, and return results, of different types; a polymorphic program is parametric if it is defined by the same type-uniform algorithm regardless of the concrete type at which it is applied. Since parametric programs can be applied to arguments of any type, they are at first glance very general. But since they cannot perform type-specific operations, their behavior is actually quite constrained. Relational parametricity formalizes the constraints on parametric programs to derive theoretically and computationally powerful results about them solely on the basis of their types. Since no knowledge whatsoever of the program text is needed to derive them, results derived from relational parametricity are sometimes playfully called 'free theorems'.
In this talk I will introduce the concept of relational parametricity, give examples of free theorems --- including optimizing program
transformations --- that are useful in programming practice, and explain why such theorems must always hold for parametric programs.
Host: Alessandra Scafuro, Chris Martens, CSC