LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 25th November 1997

Title: Elementary Proofs of Adequacy

Speaker: Ralph Loader (LFCS)

Given a denotational model of a programming language, about the first non-trivial thing one proves about the model, is computational adequacy--- that the model thinks that a program terminates if and only if the program terminates in the "real" world.

(More precisely, P is non-terminating iff P is represented in the model by an element "bottom" that is intended to represent non-termination).

Traditionally, these results are shown using logical relations. For sophisticated languages, logical relations may be hard to construct, or it may not even be clear what the appropriate notion of logical relation is.

I present an alternative proof technique, applied to Plotkin's Fixed Point Calculus (FPC). A given term can be represented using certain fixed-points. The finite iterates of the fixed-point give approximations to the original term that are finitary in a certain sense. This finitaryness is enough to establish adequacy for the approximations. In well behaved models, adequacy extends from the approximations to the original term. The proof is elementary, in that it avoids the use of abstract notions such as logical relations.