Proof-relevant parametricity

Neil Ghani; Fredrik Nordvall Forsberg; Federico Orsanigo

doi:10.1007/978-3-319-30936-1_6

Proof-relevant parametricity

Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

3 Citations (Scopus)

36 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 language	English
Title of host publication	A List of Successes That Can Change the World
Editors	Sam Lindley, Conor McBride, Phil Trinder, Don Sannella
Place of Publication	Switzerland
Publisher	Springer-Verlag
Pages	109-131
Number of pages	23
ISBN (Print)	9783319309354
DOIs	https://doi.org/10.1007/978-3-319-30936-1_6
Publication status	Published - 25 Mar 2016

Publication series

Name	Lecture Notes in Computer Science
Volume	9600
ISSN (Print)	0302-9743

Keywords

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

Access to Document

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

Ghani-etal-LNCS-2016-Proof-relevant-parametricityAccepted author manuscript, 450 KB

Cite this

@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 = mar,

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",

}

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 proceeding › Conference 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

AN - SCOPUS:84973879065

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 -

Proof-relevant parametricity

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Homotopy Type Theory: Programming and Verification

Logical Relations for Program Verification

Cite this

Proof-relevant parametricity

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Homotopy Type Theory: Programming and Verification

Logical Relations for Program Verification

Cite this