TY - RPRT
T1 - Parametric Completion for Models of Polymorphic Linear / Intuitionistic Lambda Calculus
AU - Møgelberg, Rasmus Ejlers
PY - 2005/2
Y1 - 2005/2
N2 - 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.
AB - 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.
M3 - Report
T3 - IT University Technical Report Series
BT - Parametric Completion for Models of Polymorphic Linear / Intuitionistic Lambda Calculus
PB - IT-Universitetet i København
CY - Copenhagen
ER -