Relational Parametricity and Control

Masahito Hasegawa

doi:10.2168/LMCS-2(3:3)2006

Masahito Hasegawa - Relational Parametricity and Control

lmcs:2245 - Logical Methods in Computer Science, July 27, 2006, Volume 2, Issue 3 - https://doi.org/10.2168/LMCS-2(3:3)2006

Relational Parametricity and ControlArticle

Authors: Masahito Hasegawa

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''.

Comment: 22 pages, for Logical Methods in Computer Science

https://doi.org/10.2168/LMCS-2(3:3)2006

Source: arXiv.org:cs/0606072

Volume: Volume 2, Issue 3

Secondary volumes: Selected Papers of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005)

Published on: July 27, 2006

Imported on: December 16, 2005

Keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.2

Licence: arXiv.org - Assumed non-exclusive license to distribute