  This paper introduces Hypersequent GV (HGV), a modular and extensible core
calculus for functional programming with session types that enjoys deadlock
freedom, confluence, and strong normalisation. HGV exploits hyper-environments,
which are collections of type environments, to ensure that structural
congruence is type preserving. As a consequence we obtain an operational
correspondence between HGV and HCP -- a process calculus based on hypersequents
and in a propositions-as-types correspondence with classical linear logic
(CLL). Our translations from HGV to HCP and vice-versa both preserve and
reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial
ingredient for channel forwarding and exceptions.
