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

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

Publication status | Published - 25 Mar 2016 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Volume | 9600 |

ISSN (Print) | 0302-9743 |

### Fingerprint

### Keywords

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

### Cite this

*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

}

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

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

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 -