  We consider a hierarchy of four typed call-by-value languages with either
higher-order or ground-type references and with either callcc or no control
operator.Our first result is a fully abstract trace model for the most
expressive setting, featuring both higher-order references and callcc,
constructed in the spirit of operational game semantics. Next we examine the
impact of suppressing higher-order references and callcc in contexts and
provide an operational explanation for the game-semantic conditions known as
visibility and bracketing respectively.This allows us to refine the original
model to provide fully abstract trace models of interaction with contexts that
need not use higher-order references or callcc. Along the way, we discuss the
relationship between error- and termination-based contextual testing in each
case, and relate the two to trace and complete trace equivalence
respectively.Overall, the paper provides a systematic development of
operational game semantics for all four cases, which represent the state-based
face of the so-called semantic cube.
