 The full abstraction problem has proved especially hard for a version of simply typed \(\lambda\)-calculus with arithmetic primitives called PCF (Programming with Computable Functions) (Plotkin 1977), a toy programming language based on the Logic for Computable Functions of Scott (1969) and Milner (1973). In this section we introduce (a version of) the language with its operational and denotational semantics, and outline how the full abstraction problem arises for this language. The problem has been one of the major concerns of the theoretical investigation of programming languages for about two decades, from its original formulation in the landmark papers (Milner 1977; Plotkin 1977) to the first solutions proposed in 1993 (Abramsky et al. 2000; Hyland &amp; Ong 2000) using game semantics, for which see  Section 3.