Abstract
Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambdacalculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed=functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higherdimensional relational parametricity.
Original language  English 

Title of host publication  POPL '14 Proceedings of the 41st ACM SIGPLANSIGACT 
Subtitle of host publication  Symposium on Principles of Programming Languages 
Place of Publication  New York, NY. 
Pages  503515 
Number of pages  13 
DOIs  
Publication status  Published  24 Jan 2014 
Event  POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  San Diego, United States Duration: 22 Jan 2014 → 24 Jan 2014 http://popl.mpisws.org/2014/ 
Conference
Conference  POPL 2014: 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages 

Country/Territory  United States 
City  San Diego 
Period  22/01/14 → 24/01/14 
Internet address 
Keywords
 relational parametricity
 dependent type theory
 data representations
 higherdimensional
 initial algebras
 parametric modeling
 parametric models
 reflexive graphs
Fingerprint
Dive into the research topics of 'A relationally parametric model of dependent type theory'. Together they form a unique fingerprint.Profiles

Bob Atkey
 Computer And Information Sciences  Senior Lecturer
 Mathematically Structured Programming
Person: Academic

Neil Ghani
Person: Academic