4pm Tuesday 2 October 2001
Room 2511, JCMB, King's Buildings
This talk is an overview of my thesis with the above title. The issue is step-wise refinement of abstract data type specifications, and how this concept (as originally formulated in the field of algebraic specification) might be represented and generalised in a setting consisting of the polymorphic lambda calculus together with a logic for relational parametricity a la Reynolds.
The primary idea is that this type-theoretic setting allows the refinement concept to be generalised to data types with higher-order operators. Along with this, the thesis deals with a problem of linking observational equivalence to the existence of simulation relations at higher order, as well as the problem of composability of simulation relations at higher order.
Martin Grohe
Wednesday, 17 September 2001
An error occured whilst processing this directive