Kripke Logical Relations and PCF

• To: types@dcs.gla.ac.uk
• Subject: Kripke Logical Relations and PCF
• From: ohearn@top.cis.syr.edu
• Date: Wed, 18 May 94 14:30:30 EDT
• Approved: types@dcs.gla.ac.uk

The following manuscript can is available by anonymous ftp from
top.cis.syr.edu in ohearn/pcf.dvi or ohearn/pcf.ps.


		 Kripke Logical Relations and PCF
		Peter W. O'Hearn and Jon G. Riecke

ABSTRACT: Sieber has described a model of PCF consisting of
continuous functions that are invariant under certain (finitary)
logical relations, and shown that it is fully abstract up to rank
three types.  We show that one may achieve full abstraction at ALL
types using a form of ``Kripke logical relations'' introduced by
Jung and Tiuryn to characterize lambda-definability.

• Prev: paper available (draft)
• Next: School on Typed Lambda Calculus ( final announcement )
• Index(es):
  • Main
  • Thread