Proof-relevant parametricity

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

2 Citations (Scopus)
12 Downloads (Pure)

Abstract

Parametricity is one of the foundational principles which underpin our understanding of modern programming languages. Roughly speaking, parametricity expresses the hidden invariants that programs satisfy by formalising the intuition that programs map related inputs to related outputs. Traditionally parametricity is formulated with proofirrelevant relations but programming in Type Theory requires an extension to proof-relevant relations. But then one might ask: can our proofs that polymorphic functions are parametric be parametric themselves? This paper shows how this can be done and, excitingly, our answer requires a trip into the world of higher dimensional parametricity.

Original languageEnglish
Title of host publicationA List of Successes That Can Change the World
EditorsSam Lindley, Conor McBride, Phil Trinder, Don Sannella
Place of PublicationSwitzerland
PublisherSpringer-Verlag
Pages109-131
Number of pages23
ISBN (Print)9783319309354
DOIs
Publication statusPublished - 25 Mar 2016

Publication series

NameLecture Notes in Computer Science
Volume9600
ISSN (Print)0302-9743

Keywords

  • computer science
  • computers
  • higher-dimensional
  • parametricity
  • polymorphic functions
  • relevant relations
  • type theory
  • artificial intelligence

Fingerprint Dive into the research topics of 'Proof-relevant parametricity'. Together they form a unique fingerprint.

  • Projects

  • Cite this

    Ghani, N., Nordvall Forsberg, F., & Orsanigo, F. (2016). Proof-relevant parametricity. In S. Lindley, C. McBride, P. Trinder, & D. Sannella (Eds.), A List of Successes That Can Change the World (pp. 109-131). (Lecture Notes in Computer Science; Vol. 9600). Switzerland: Springer-Verlag. https://doi.org/10.1007/978-3-319-30936-1_6