##
Logical Relations and Parametricity:
A Reynolds Programme for Category Theory and Programming Languages

### Uday S. Reddy

###
(Dedicated to the memory of John Reynolds, 1935-2013)

In his seminal paper on "Types, Abstraction and Parametric Polymorphism,"
John Reynolds called for homomorphisms to be generalized from functions to
relations. He reasoned that such a generalization would allow type-based
"abstraction" (representation independence, information hiding, naturality
or parametricity) to be captured in a mathematical theory, while accounting
correctly for higher-order types. However, after 30 years of research, we
do not yet know fully how to do such a generalization. In this talk, I
interpret Reynolds's insights for the broad scope of mathematics and
science, indicate what shape a general theory based on the insights might
take, and summarize the work carried out so far.

[An article outline of these ideas, joint with Claudio Hermida and Edmund
Robinson, may be found at http://www.cs.bham.ac.uk/~udr.]