# zbMATH — the first resource for mathematics

Relational parametricity and control. (English) Zbl 1126.68023
Summary: 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”.

##### MSC:
 68N18 Functional programming and lambda calculus 03B40 Combinatory logic and lambda calculus
Full Text: