Paper: Relational Parametricity and Control (at LICS 2005)

Authors: Masahito Hasegawa

Abstract

We study the equational theory of Parigot’s secondorder ?µ-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."

BibTeX

  @InProceedings{Hasegawa-RelationalParametri,
    author = 	 {Masahito Hasegawa},
    title = 	 {Relational Parametricity and Control},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {72--81},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }