Projects per year
Abstract
This paper combines reflexivegraphcategory 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 reflexivegraphcategory structure, enjoy the expected consequences of parametricity. This is proved using a typetheoretic presentation of the categorytheoretic 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.
Original language  English 

Title of host publication  International Conference on Foundations of Software Science and Computation Structures [FoSSaCS 2016] 
Editors  Bart Jacobs, Christof Löding 
Place of Publication  Berlin 
Publisher  SpringerVerlag 
Pages  319 
Number of pages  17 
Volume  9634 
ISBN (Electronic)  9783662496305 
ISBN (Print)  9783662496299 
DOIs  
Publication status  Published  22 Mar 2016 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer Berlin Heidelberg 
ISSN (Print)  03029743 
Keywords
 polymorphism
 re exivegraphcategory structure
 parametricity
 impredicative polymorphism
 type theory
Fingerprint
Dive into the research topics of 'Comprehensive parametric polymorphism: categorical models and type theory'. Together they form a unique fingerprint.Profiles
Projects
 2 Finished

Homotopy Type Theory: Programming and Verification
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research

Logical Relations for Program Verification
EPSRC (Engineering and Physical Sciences Research Council)
30/09/13 → 29/09/17
Project: Research
Prizes

ETAPS 2016 EATCS best paper award
Nordvall Forsberg, Fredrik (Recipient), Ghani, Neil (Recipient) & Simpson, A. (Recipient), 6 Apr 2016
Prize: Prize (including medals and awards)