 This gives us the necessary terminology to understand the statement of the intensional full abstraction theorem proved in Hyland &amp; Ong 2000 (th. 7.1), where the types of PCF are interpreted as games and terms as innocent and well-bracketed strategies, see also Abramsky et al. 2000 (th. 3.2), Curien 2006 (th. 5.1):