Cryptography is information hiding.  Polymorphism is also information
hiding.  So is cryptography polymorphic?  Is polymorphism
cryptographic?

To investigate these questions, we define the _cryptographic
lambda-calculus_, a simply typed lambda-calculus with shared-key
cryptographic primitives.  Although this calculus is simply typed, it
is powerful enough to encode recursive functions, recursive types, and
dynamic typing.  We then develop a theory of relational parametricity
for our calculus as Reynolds did for the polymorphic lambda-calculus.
This theory is useful for proving equivalences in our calculus; for
instance, it implies the non-interference property: values encrypted
by a key cannot be distinguished from one another by any function
ignorant of the key.  We close with an encoding of the polymorphic
lambda-calculus into the cryptographic calculus that uses cryptography
to protect type abstraction.

Our results shed a new light upon the relationship between
cryptography and polymorphism, and offer a first step toward extending
programming idioms based on type abstraction (such as modules and
packages) from the civilized world of polymorphism, where only
well-typed programs are allowed, to the unstructured world of
cryptography, where friendly programs must cohabit with malicious
attackers.