  Session types have emerged as a typing discipline for communication
protocols. Existing calculi with session types come equipped with many
different primitives that combine communication with the introduction or
elimination of the transmitted value.
  We present a foundational session type calculus with a lightweight
operational semantics. It fully decouples communication from the introduction
and elimination of data and thus features a single communication reduction,
which acts as a rendezvous between senders and receivers. We achieve this
decoupling by introducing label-dependent session types, a minimalist
value-dependent session type system with subtyping. The system is sufficiently
powerful to simulate existing functional session type systems. Compared to such
systems, label-dependent session types place fewer restrictions on the code. We
further introduce primitive recursion over natural numbers at the type level,
thus allowing to describe protocols whose behaviour depends on numbers
exchanged in messages. An algorithmic type checking system is introduced and
proved equivalent to its declarative counterpart. The new calculus showcases a
novel lightweight integration of dependent types and linear typing, with has
uses beyond session type systems.
