We present a programming model and typing discipline for complex multi-robot coordination programming.
Our model encompasses both synchronisation through message passing and continuous-time
dynamic motion primitives in physical space.
We specify <i>continuous-time motion primitives</i> in an assume-guarantee
logic that ensures compatibility of motion primitives as well as collision freedom.
We specify global behaviour of programs in a <i>choreographic</i> type system that extends
multiparty session types with jointly executed motion primitives, predicated refinements,
as well as a <i>separating conjunction</i> that allows reasoning about subsets of interacting
robots.
We describe a notion of <i>well-formedness</i> for global types
that ensures motion and communication can be correctly synchronised and provide algorithms for
checking well-formedness, projecting a type, and local type checking.
A well-typed program is <i>communication safe</i>, <i>motion compatible</i>, and <i>collision free</i>.
Our type system provides a compositional approach to ensuring these properties.

We have implemented our model on top of the ROS framework.
This allows us to program multi-robot coordination scenarios
on top of commercial and custom robotics hardware platforms.
We show through case studies that we can model and statically verify quite
complex manoeuvres involving multiple manipulators and mobile robots—such
examples are beyond the scope of previous approaches.