Relational parametricity and control (extended abstract).

Masahito Hasegawa

In Proc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS2005), Chicago


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.

Back to Hassei's Research Page / Home Page