Proof-relevant parametricity

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

2 Citations (Scopus)

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.

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

Fingerprint

Computer programming languages
Type Theory
Programming Languages
High-dimensional
Express
Programming
Invariant
Output

Keywords

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

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
Ghani, Neil ; Nordvall Forsberg, Fredrik ; Orsanigo, Federico. / Proof-relevant parametricity. A List of Successes That Can Change the World. editor / Sam Lindley ; Conor McBride ; Phil Trinder ; Don Sannella. Switzerland : Springer-Verlag, 2016. pp. 109-131 (Lecture Notes in Computer Science).
@inproceedings{04e1ef339a3d4ce488242a8481a5deda,
title = "Proof-relevant parametricity",
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.",
keywords = "computer science, computers, higher-dimensional, parametricity, polymorphic functions, relevant relations, type theory, artificial intelligence",
author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Federico Orsanigo",
note = "This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science. The final authenticated version is available online at: https://doi.org/10.1007/978-3-319-30936-1_6",
year = "2016",
month = "3",
day = "25",
doi = "10.1007/978-3-319-30936-1_6",
language = "English",
isbn = "9783319309354",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
pages = "109--131",
editor = "Sam Lindley and Conor McBride and Phil Trinder and Don Sannella",
booktitle = "A List of Successes That Can Change the World",

}

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. Lecture Notes in Computer Science, vol. 9600, Springer-Verlag, Switzerland, pp. 109-131. https://doi.org/10.1007/978-3-319-30936-1_6

Proof-relevant parametricity. / Ghani, Neil; Nordvall Forsberg, Fredrik; Orsanigo, Federico.

A List of Successes That Can Change the World. ed. / Sam Lindley; Conor McBride; Phil Trinder; Don Sannella. Switzerland : Springer-Verlag, 2016. p. 109-131 (Lecture Notes in Computer Science; Vol. 9600).

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

TY - GEN

T1 - Proof-relevant parametricity

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Orsanigo, Federico

N1 - This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science. The final authenticated version is available online at: https://doi.org/10.1007/978-3-319-30936-1_6

PY - 2016/3/25

Y1 - 2016/3/25

N2 - 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.

AB - 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.

KW - computer science

KW - computers

KW - higher-dimensional

KW - parametricity

KW - polymorphic functions

KW - relevant relations

KW - type theory

KW - artificial intelligence

UR - http://www.scopus.com/inward/record.url?scp=84973879065&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-30936-1_6

DO - 10.1007/978-3-319-30936-1_6

M3 - Conference contribution book

SN - 9783319309354

T3 - Lecture Notes in Computer Science

SP - 109

EP - 131

BT - A List of Successes That Can Change the World

A2 - Lindley, Sam

A2 - McBride, Conor

A2 - Trinder, Phil

A2 - Sannella, Don

PB - Springer-Verlag

CY - Switzerland

ER -

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