"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.
Reference material