Relational Parametricity and Control
<|reference_start|>Relational Parametricity and Control: 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''.<|reference_end|>
@article{hasegawa2006relational,
    title={Relational Parametricity and Control},
    author={Masahito Hasegawa},
    journal={Logical Methods in Computer Science, Volume 2, Issue 3 (July 27,
  2006) lmcs:2245},
    year={2006},
    doi={10.2168/LMCS-2(3:3)2006},
    archivePrefix={arXiv},
    eprint={cs/0606072},
    primaryClass={cs.PL cs.LO}
}