Universal properties for universal types in bifibrational parametricity

Research output: Contribution to journalArticle

4 Downloads (Pure)

Abstract

In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.
Original languageEnglish
Pages (from-to)810–827
Number of pages18
JournalMathematical Structures in Computer Science
Volume29
Issue number6
Early online date22 Mar 2019
DOIs
Publication statusPublished - 30 Jun 2019

Keywords

  • categorical semantics
  • comprehension categories
  • relational parametricity

Fingerprint Dive into the research topics of 'Universal properties for universal types in bifibrational parametricity'. Together they form a unique fingerprint.

  • Parametric polymorphism - universally

    Ghani, N., Nordvall Forsberg, F. & Orsanigo, F., 24 Jun 2015, Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. de Paiva, V., de Queiroz, R., Moss, L. S., Leivant, D. & de Oliveira, A. G. (eds.). p. 81-92 12 p. (Lecture Notes in Computer Science; vol. 9160).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution book

    Open Access
    File
    5 Citations (Scopus)
    140 Downloads (Pure)

Cite this