Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Rasmus Ejlers Møgelberg, Denmark
  • Lars Birkedal
  • Guiseppe Rosolini, Italy
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
Issue2
Pages (from-to)115-133
Number of pages19
ISSN0168-0072
Publication statusPublished - 2 Sep 2008
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743248