TL;DR
This paper explores the connection between relational parametricity and control operators in the λμ-calculus, proposing a constrained form called 'focal parametricity' to align semantics with CPS translations.
Contribution
It introduces 'focal parametricity' as a constrained relational parametricity framework for λμ-calculus, reconciling parametricity with control operators and CPS semantics.
Findings
Relational parametricity induces a natural equivalence on λμ-terms.
Unconstrained parametricity is inconsistent with CPS semantics.
Focal parametricity provides a consistent framework for parametricity with control.
Abstract
We study the equational theory of Parigot's second-order λμ-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment of the second-order λ-calculus. It is observed that the relational parametricity on the target calculus induces a natural notion of equivalence on the λμ-terms. On the other hand, the unconstrained relational parametricity on the λμ-calculus turns out to be inconsistent with this CPS semantics. Following these facts, we propose to formulate the relational parametricity on the λμ-calculus in a constrained way, which might be called ``focal parametricity''.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.