Comprehensive parametric polymorphism : categorical models and type theory

Tools

Ghani, Neil and Nordvall Forsberg, Fredrik and Simpson, Alex; Jacobs, Bart and Löding, Christof, eds. (2016) Comprehensive parametric polymorphism : categorical models and type theory. In: International Conference on Foundations of Software Science and Computation Structures [FoSSaCS 2016]. Lecture Notes in Computer Science, 9634 . Springer-Verlag, Berlin, pp. 3-19. ISBN 9783662496305 (https://doi.org/10.1007/978-3-662-49630-5_1)

[thumbnail of Ghani-etal-FOSSACS2016-comprehensive-parametric-polymorphism-categorical-models-type-theory]
Preview
 Text. Filename: Ghani_etal_FOSSACS2016_comprehensive_parametric_polymorphism_categorical_models_type_theory.pdf
Accepted Author Manuscript
Download (423kB)| Preview

Abstract

This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.

ORCID iDs

Ghani, Neil ORCID logoORCID: https://orcid.org/0000-0002-3988-2560, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Simpson, Alex; Jacobs, Bart and Löding, Christof
  • Item type:Book Section
    ID code:56242
    Dates:
    Date
    Event
    22 March 2016
    Published
    18 December 2015
    Accepted
    Notes:The final publication is available at Springer via https://doi.org/10.1007/978-3-662-49630-5_1
    Subjects:Science > Mathematics > Computer software
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:28 Apr 2016 15:17
    Last modified:12 Dec 2024 01:11
    URI:https://strathprints.strath.ac.uk/id/eprint/56242
CORE (COnnecting REpositories)