Relating full abstraction results for different programming languages

Abstract

We prove that Plotkin’s model of bottomless epos and partial continuous functions [19] is fully abstract for PCFv, a call-by-yalue version of the language PCF [17]. This settles a ‘folk theorem’ which has occasionally been misunderstood. We then show that the (known) full abstraction results for lazy PCF [2] and PCF with control [22] can be derived as corollaries from this theorem. Such a connection is particularly surprising, because observational congruence-the central notion in the definition of full abstraction-is usually not preserved by many known translations between different programming languages. We expect that new full abstraction theorems for some extensions of PCFv can be derived in the same way.