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

- Slides: Lecture 1
- Slides: Lecture 2
- Exercise Sheet 1
- Slides: Lecture 4 on Axiomatic Theory
- Working notes on Relational Categories

- Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming languages by C. Hermida, U. S. Reddy and E. P. Robinson. WACT 2013.
- Lambda Definability and Logical Relations, by G. Plotkin (1973 Tech. Report) and Lambda Definability in the Full Type Hierarchy, by G. Plotkin (1980)
- Types, Abstraction and Parametric Polymorphism, by J. Reynolds (1983)
- A Logic for Parametric Polymorphism, G. Plotkin and M. Abadi (1993).
- Parametricity and Local Variables, by P. W. O'Hearn and R. D. Tennent (1995).
- Structural Inducation and Coinductin in a Fibrational Setting, C. Hermida and B. Jacobs (1998).

Last modified: Sat Apr 26 19:0:00 GMT 2014