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


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
Issue number2
Pages (from-to)115-133
Number of pages19
Publication statusPublished - 2 Sept 2008

Cite this