Projects per year
Abstract
Reynolds’ relational parametricity provides a powerful way to rea son about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ the ory exists, exploiting invariance to yield “free theorems”, non inhabitation results, and encodings of algebraic datatypes. Outside computer science, invariance is a common theme running through many areas of mathematics and physics. For example, the area of a triangle is unaltered by rotation or flipping. If we scale a trian gle, then we scale its area, maintaining an invariant relationship be tween the two. The transformations under which properties are in variant are often organised into groups, with the algebraic structure reflecting the composability and invertibility of transformations. In this paper, we investigate programming languages whose types are indexed by algebraic structures such as groups of ge ometric transformations. Other examples include types indexed by principals–for information flow security–and types indexed by distances–for analysis of analytic uniform continuity properties. Following Reynolds, we prove a general Abstraction Theorem that covers all these instances. Consequences of our Abstraction Theo rem include free theorems expressing invariance properties of pro grams, type isomorphisms based on invariance properties, and non definability results indicating when certain algebraically indexed types are uninhabited or only inhabited by trivial programs. We have fully formalised our framework and most examples in Coq.
Original language  English 

Title of host publication  Proceedings of the 40th annual ACM SIGPLANSIGACT symposium on Principles of programming languages 
Subtitle of host publication  POPL '13 
Editors  Roberto Giacobazzi, Radhia Cousot 
Pages  87100 
Number of pages  14 
DOIs  
Publication status  Published  Jan 2013 
Event  Proceedings of the 40th ACM SIGACTSIGPLAN Symposium, POPL 2013.  Rome, United Kingdom Duration: 23 Sep 2013 → 25 Sep 2013 
Conference
Conference  Proceedings of the 40th ACM SIGACTSIGPLAN Symposium, POPL 2013. 

Country  United Kingdom 
City  Rome 
Period  23/09/13 → 25/09/13 
Keywords
 abstraction
 invariance
 algebraically indexed types
Projects
 1 Finished

Categorical Foundations of Indexed Programming
Johann, P. & Ghani, N.
EPSRC (Engineering and Physical Sciences Research Council)
1/07/09 → 31/12/12
Project: Research