Characteristic bisimulation for higher-order session processes (Q2357655)

For higher-order (process) languages, characterizing contextual equivalence is a long-standing problem. In the setting of a higher-order \(\pi\)-calculus with session types, characteristic bisimilarity, a typed bisimilarity which fully characterizes contextual equivalence, is developed. Using simple values inhabiting (session) types, this approach differs from untyped methods for characterizing contextual equivalence in higher-order processes. It is shown that considering as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. It is demonstrated how characteristic bisimilarity can be used to justify optimizations in session protocols with mobile code communication.