Parametric Completion for Models of Polymorphic Linear / Intuitionistic Lambda Calculus

TR-2005-60, Author: Rasmus Ejlers Møgelberg

Rasmus Ejlers Møgelberg

February 2005

Abstract

We show how the externalization of an internal PILLY-model in a quasi-topos gives rise to a canonical pre-LAPL-structure in which the logic is the internal logic of the quasi-topos. This corresponds to how one intuitively would think of parametricity for such internal models. We describe a parametric completion process which takes an internal model of PILLY in a quasi-topos and builds a new internal PILLY-model in a presheaf topos over the original quasi-topos. The externalization of this PILLY-model extends to a full parametric LAPL-structure. However, this LAPL-structure is different from the canonical one, since the logic comes from the original quasi-topos.
This paper assumes knowledge of LAPL-structures.

---

Technical report TR-2005-60 in IT University Technical Report Series,
February 2005.
Available as PDF.