Relational Parametricity for Control Considered as a Computational Effect

Rasmus Mogelberg, Alexander Simpson

Research output: Contribution to journalArticlepeer-review


This paper investigates parametric polymorphism in the presence of control operators. Our approach is to specialise a general type theory combining polymorphism and computational effects, by extending it with additional constants expressing control. By defining relationally parametric models of this extended calculus, we capture the interaction between parametricity and control. As a worked example, we show that recent results of M. Hasegawa on type definability in the second-order (call-by-name) λμ-calculus arise as special cases of general results valid for arbitrary computational effects.
Original languageEnglish
Pages (from-to)295-312
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2007


Dive into the research topics of 'Relational Parametricity for Control Considered as a Computational Effect'. Together they form a unique fingerprint.

Cite this