### Abstract

Original language | English |
---|---|

Title of host publication | Foundations of Software Science and Computation Structures |

Subtitle of host publication | 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings |

Editors | Bart Jacobs, Christof Löding |

Pages | 3-19 |

Number of pages | 17 |

Volume | 9634 |

ISBN (Electronic) | 978-3-662-49630-5 |

DOIs | |

Publication status | Published - 22 Mar 2016 |

### Publication series

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

Publisher | Springer Berlin Heidelberg |

ISSN (Print) | 0302-9743 |

### Fingerprint

### Keywords

- polymorphism
- re exive-graph-category structure
- parametricity
- impredicative polymorphism
- type theory

### Cite this

*Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings*(Vol. 9634, pp. 3-19). (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-49630-5_1

}

*Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings.*vol. 9634, Lecture Notes in Computer Science, pp. 3-19. https://doi.org/10.1007/978-3-662-49630-5_1

**Comprehensive parametric polymorphism : categorical models and type theory.** / Ghani, Neil; Nordvall Forsberg, Fredrik; Simpson, Alex.

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

TY - GEN

T1 - Comprehensive parametric polymorphism

T2 - categorical models and type theory

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Simpson, Alex

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49630-5_1

PY - 2016/3/22

Y1 - 2016/3/22

N2 - This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.

AB - This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.

KW - polymorphism

KW - re exive-graph-category structure

KW - parametricity

KW - impredicative polymorphism

KW - type theory

UR - http://www.etaps.org/index.php/2016/fossacs

U2 - 10.1007/978-3-662-49630-5_1

DO - 10.1007/978-3-662-49630-5_1

M3 - Conference contribution book

SN - 978-3-662-49629-9

VL - 9634

T3 - Lecture Notes in Computer Science

SP - 3

EP - 19

BT - Foundations of Software Science and Computation Structures

A2 - Jacobs, Bart

A2 - Löding, Christof

ER -