In this project, we seek to apply principles from the field of programming languages to distributed robotics. The essence of programming languages is to design simple APIs that support compositional reasoning. We embrace that philosophy through tools from programming languages such as type theory and proof assistants to produce correct-by-construction programs that control teams of robots coordinating their actions to achieve complex tasks.
