This work proposes tractable bisimulations for the higher-order -
calculus with session primitives (HO ) and o ers a complete study of the expressivity
of its most significant subcalculi. First we develop three typed bisimulations,
which are shown to coincide with contextual equivalence. These characterisations
demonstrate that observing as inputs only a specific finite set of
higher-order values (which inhabit session types) su ces to reason about HO
processes. Next, we identify HO, a minimal, second-order subcalculus of HO
in which higher-order applications/abstractions, name-passing, and recursion are
absent. We show that HO can encode HO extended with higher-order applications
and abstractions and that a first-order session -calculus can encode HO .
Both encodings are fully abstract. We also prove that the session -calculus with
passing of shared names cannot be encoded into HO without shared names. We
show that HO , HO, and are equally expressive; the expressivity of HO enables
e ective reasoning about typed equivalences for higher-order processes.