From parametric polymorphism to models of polymorphic FPC

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

    Abstract

    This paper shows how parametric PILL Y (Polymorphic Intuitionistic / Linear Lambda calculus with a fixed point combinator Y) can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using recent results about solutions to recursive domain equations in parametric models of PILL Y , we show how to interpret FPC in these. Of particular interest is a model based on “admissible” pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is the first model of a language with parametric polymorphism, recursive terms and recursive types in a non-linear setting.

    Original languageEnglish
    JournalMathematical Structures in Computer Science
    Volume19
    Issue number4
    Pages (from-to)639-686
    ISSN0960-1295
    Publication statusPublished - 2009

    Keywords

    • Parametric PILL Y
    • Polymorphic Intuitionistic Lambda Calculus
    • Fixed Point Combinator Y
    • Domain Theory
    • Recursive Domain Equations

    Fingerprint

    Dive into the research topics of 'From parametric polymorphism to models of polymorphic FPC'. Together they form a unique fingerprint.

    Cite this