@book{9e6f517ee22d4f4ab4d21b03468eea26,
title = "Parametric Completion for Models of Polymorphic Linear / Intuitionistic Lambda Calculus",
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.",
keywords = "PILLY-model, quasi-topos, parametricity, presheaf topos, LAPL-structure",
author = "M{\o}gelberg, \{Rasmus Ejlers\}",
year = "2005",
month = feb,
language = "English",
series = "IT University Technical Report Series",
number = "TR-2005-60",
publisher = "IT-Universitetet i K{\o}benhavn",
address = "Denmark",
edition = "TR-2005-60",
}