Logical relations and parametricity

Uday Reddy (Birmingham)

"Logical relations" and "relational parametricity," twin theories developed by Gordon Plotkin and John Reynolds, constitute a theory of types covering higher-order functions. The theory has a wide range of applications, including proofs of program equivalence and bisimulation, data abstraction and information hiding, generic functions and parametric polymorphism, structural induction and coinduction, and proofs of compiler correctness. This course is a gentle introduction to the theory along with an exploration of some of the applications.

Lectures

Reference material

Back to MGS 2014
Last modified: Sat Apr 26 19:0:00 GMT 2014