COMPUTER SCIENCE COLLOQUIUM

Lars Birkedal Theory Department IT University of Copenhagen

Tuesday, April 19, 2005, at 14:15 Seminar Room

ABSTRACT

We present a formalization of a linear version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic / linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including solutions to recursive domain equations. We further define a notion of parametric LAPL-structure and prove that it provides a sound and complete class of models for the logic. Finally, we present a concrete parametric parametric LAPL-structure based on suitable categories of partial equivalence relations over a universal model of the untyped lambda calculus.

Host: Klaus Meer

---

SDU HOME | IMADA HOME | Previous Page

---

Last modified: Wed Apr 6 08:35:26 CEST 2005

Joan Boyar (joan@imada.sdu.dk)