Personal tools
You are here: Home Events Abstract Archives 2001 Abstraction Barriers and Refinement in the Polymorphic Lambda Calculus

Abstraction Barriers and Refinement in the Polymorphic Lambda Calculus

Jo Hannay LFCS 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.

Document Actions