LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 27th January 1998

Title: Parametric polymorphism and operational equivalence

Speaker: Andrew Pitts (University of Cambridge)

Studies of the mathematical properties of impredicatively polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard-Reynolds, which is a calculus of total polymorphic functions. This talk considers polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (`lazy') datatypes. An operationally-based approach to Reynolds' notion of relational parametricity is developed for an extension of Plotkin's PCF with universally quantified types and lazy lists. The resulting logical relation is shown to be a useful tool for proving properties of polymorphic types up to a notion of operational equivalence based on Morris-style contextual equivalence.

Further details