Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

Semantics of Computation Seminar

Friday October 27, 2:15 pm

Kripke Logical Relations and PCF

Jon G. Riecke
AT&T Bell Laboratories

Abstract: The nature of sequential functional computution has fascinated computer scientists ever since Dana Scott remarked on a urious incompleteness phenomenon when he introduced LCF and its continuous function model in 1969. Although the functionals definable by terms in PCF---the term language of LCF---admitted a sequential evaluation strategy, there were functions in the model that could only be implemented in a parallel fashion. The problem of giving a semantic description of the notion of a "sequentially computable functional" has remained a notorious open problem since then.

This talk sketches a new model of PCF that consists of continuous unctions that are invariant under a certain form of "Kripke logical relation." [This builds on previous work of Sieber, and Jung and Tiuryn.] The main result is that the model is fully abstract. We briefly compare our results to the recent "game semantics" of Abramsky-Jagadeesan-Malacaria, Hyland-Ong, and Nickau, and describe why we feel the "full abstraction" problem for PCF may not be solved yet.

This is joint work with Peter W. O'Hearn.

Copyright © Isaac Newton Institute