### Relational parametricity and control (extended abstract).

Masahito Hasegawa

### Abstract

We study the equational theory of Parigot's second-order $\lambda\mu$-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment of the second-order $\lambda$-calculus. It is observed that the relational parametricity on the target calculus induces a natural notion of equivalence on the $\lambda\mu$-terms. On the other hand, the unconstrained relational parametricity on the $\lambda\mu$-calculus turns out to be inconsistent with this CPS semantics. Following these facts, we propose to formulate the relational parametricity on the $\lambda\mu$-calculus in a constrained way, which might be called focal parametricity''.

There is a missing condition in the definition of "P-focality" in Section 5.2. Please have a look at the revised version appeared in Logical Methods in Computer Science, 2(3:3):1-22.