Relational parametricity and control (extended abstract).
Masahito Hasegawa
In
Proc. 20th
Annual IEEE Symposium on Logic in Computer Science (LICS2005), Chicago
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.
Back to Hassei's
Research Page / Home Page