Abstract: Relational parametricity is a key technique for reasoning about programs in strongly typed languages. It is a powerful principle for

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.

Short Bio: I am a (Full) Professor in the Computer Science Department at Appalachian State University in Boone, NC, where I do research and teach a variety of computer science courses. Before coming to Appalachian State University, I was a Reader (US equivalent: Professor) of Computer Science in the Mathematically Structured Programming group in the Department of Computer and Information Sciences at the University of Strathclyde in Glasgow, Scotland. While there I spent part of a sabbatical in 2012 at the Department of Computer Science and Engineering at Chalmers University in Gothenburg, Sweden.