  Concurrent distributed systems are notoriously difficult to construct and
reason about. Choreographic programming is a recent paradigm that describes a
distributed system in a single global program called a choreography.
Choreographies simplify reasoning about distributed systems and can ensure
deadlock freedom by static analysis. In previous choreographic programming
languages, each value is located at a single party, and the programmer is
expected to insert special untyped "select" operations to ensure that all
parties follow the same communication pattern.
  We present He-Lambda-Small, a new choreographic programming language with
Multiply Located Values. He-Lambda-Small allows multicasting to a set of
parties, and the resulting value will be located at all of them. This approach
enables a simple and elegant alternative to "select": He-Lambda-Small requires
that the guard for a conditional be located at all of the relevant parties. In
He-Lambda-Small, checking that a choreography is well-typed suffices to show
that it is deadlock-free. We present several case studies that demonstrate the
use of multiply-located values to concisely encode tricky communication
patterns described in previous work without the use of "select" or redundant
communication.
