Relational parametricity for control considered as a computational effect

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

    Abstract

    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 languageDanish
    JournalElectronical Notes in Theoretical Computer Science
    Volume173
    ISSN1571-0661
    Publication statusPublished - 2007

    Keywords

    • Computational effects
    • control
    • denotational semantics
    • parametric polymorphism

    Cite this