| |
VOLUME 2, ISSUE 3, PAPER 3
|
Relational Parametricity and Control
|
©Masahito Hasegawa, Kyoto University
|
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''.
|
Publication date: July 27, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(3:3)2006
Hit Counts: 5270 |
 Creative Commons | |
