SHF: Small: Open Choreographies via Session Types

Programming concurrent and distributed systems is notoriously difficult and error prone. Since most concurrent and distributed programs are designed as a set of communicating components, incorrect communication protocols can lead to difficult-to-debug errors. Choreographic programming is a recent programming paradigm which helps developers codesign computations, thereby eliminating the possibility of errors within communication protocols.

Unfortunately, choreographic programs require that all components are programmed at the same time, preventing the use of off-the-shelf software. This project develops open choreographies: choreographies that allow codesigned components to communicate with independently designed programs. This project's novelties are the invention of open choreographies and the development of a method for expressing the protocols they expect of the non-codesigned programs.

This project’s impacts are allowing the development of correct distributed and concurrent systems that can integrate into standard software development workflows. This project’s educational impacts include the training of PhD researchers as well as experiential learning and research opportunities through the University at Buffalo’s experiential learning and research program for undergraduates.

In particular, this project develops a new session typing discipline called scheduled session types which describe the protocols of concurrent software. This session typing discipline is then used to describe how the codesigned components of a choreography interact with other components. By proving that every concurrent program that has a session type cannot have any protocol errors, we can then know that any open choreography can interact with independently designed programs without protocol errors.

By synthesizing session types from a choreography, we can make this guarantee without the programmer having to understand session types. Thus, programmers can use choreographies to develop concurrent and distributed programs without fear, and without needing to understand arcane new type-theoretic techniques.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.