2pm Friday 2nd December 2005
Room 2511, JCMB, King's Buildings
Abstract: It was first realized by Gordon Plotkin, that if one combines parametric polymorphism with recursion for terms, one obtains a strong type theory in which one can find solutions to recursive type equations. He also realized, however, that one must be careful when doing so, as if the parametricity principle becomes too strong, the theory collapses. In a talk more than ten years ago, he suggested studying a type theory with linear as well as intuitionistic variables, polymorphism and fixed points, with a logic for reasoning using parametricity.
In my PhD dissertation, I have, in collaboration with my supervisor Lars Birkedal and fellow student Rasmus Lerchedahl Petersen, presented such a logic based on Plotkins sketch. The logic contains an axiomatisation of a notion of admissible relations, which serves to weaken the parametricity principle enough to obtain non-trivial models.
The talk will give an overview of the logic, show how to solve domain equations using parametricity, and, if time permits, I will describe reasoning principles for the obtained recursive types.