some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

      Issue 5

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

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: 9276

Creative Commons