Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic

Rasmus Ejlers Møgelberg, Lars Birkedal, Guiseppe Rosolini

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

    Abstract

    Plotkin suggested using a polymorphic dual intuitionistic/linear type theory (PILLY ) as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of PILLY , in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin. In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo’s language Lily into synthetic domain theory presented by Simpson and Rosolini gives rise to a parametric LAPL-structure. This adds to the evidence that the notion of LAPL-structure is a general notion, suitable for treating many different parametric models, and it provides formal proofs of consequences of parametricity expected to hold for the interpretation. Finally, we show how these results, in combination with Rosolini and Simpson’s computational adequacy result, can be used to prove consequences of parametricity for Lily. In particular, we show that one can solve domain equations in Lily up to ground contextual equivalence
    Original languageEnglish
    JournalAnnals of Pure and Applied Logic
    Volume155
    Issue number2
    Pages (from-to)115-133
    Number of pages19
    ISSN0168-0072
    Publication statusPublished - 2 Sept 2008

    Keywords

    • Parametric polymorphism
    • Intuitionistic set theory
    • Domain theory
    • Linear lambda calculus

    Fingerprint

    Dive into the research topics of 'Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic'. Together they form a unique fingerprint.

    Cite this