Session types codify the structure of communication, making software more reliable and easier to construct.
Concurrency and distribution are computing's most pressing problem. As we approach the 50th anniversary of Moore's Law, the rules are changing: processor core counts are doubling while clock speeds remain fixed, rendering exploitation of concurrency essential. Meanwhile, we have entered an age where everyone has a computer in their pocket, depending crucially on communication with other computers to achieve their function. Without a way to routinely and reliably build concurrent and distributed systems, a half century of unprecedented technical progress will draw to a close.
The data type is one of computing's most successful ideas. The notion of data type appears in programming languages from the oldest to the newest, and covers concepts ranging from a single bit to organised tables containing petabytes of data. Types act as the fundamental unit of compositionality: the first thing a programmer writes or reads about each method or module is the data types it acts upon, and type discipline guarantees that each call of a method matches its definition and each import of a module matches its export. Data types play a central role in all aspects of software, from architectural design to interactive development environments to efficient compilation.
Session types will play a crucial role in all aspects of software. Today, architects model systems using types that are directly supported in the programming language, whereas they model communications using protocols that have no direct support in the programming language; tomorrow, they will model communication using session types that are directly supported in the programming language. Today, programmers use interactive development environments that prompt for methods based on types, and give immediate feedback indicating where code violates type discipline, whereas they have no similar support for coding communications; tomorrow, interactive development environments will prompt for messages based on session types, and give immediate feedback indicating where code violates session type discipline. Today, software tools exploit types to optimise code, whereas they do not exploit protocols; tomorrow, software tools will exploit session types to optimise communication. In short, architects, programmers, and software tools will all be aided by session types to reduce the cost of producing concurrent and distributed software, while increasing its reliability and efficiency.
ABCD is an EPSRC programme grant, funded May 2013—May 2018.
Sam Lindley, J. Garrett Morris. Sessions as Propositions. PLACES 2014.
Nicholas Ng, Nobuko Yoshida. Pabble: Parameterised Scribble for Parallel Programming. PDP 2014.
Nobuko Yoshida, Raymond Hu, Rumyana Neykova, Nicholas Ng. The Scribble Protocol Language.TGC 2013.
Fabrizio Montesi, Nobuko Yoshida. Compositional Choreographies. CONCUR 2013: 439 - 425.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions.MSCS.
Dimitrios Kouzapas, Nobuko Yoshida. Globally Governed Session Semantics. CONCUR 2013: 409-395.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, Nobuko Yoshida. Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions. COORDINATION 2013: 45-59.
Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, Nobuko Yoshida. Monitoring Networks through Multiparty Session Types. FMOODS/FORTE 2013: 50 - 65.
Pierre-Malo Deniléou, Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types.ICALP 2013: 174-186.
Raymond Hu, Rumyana Neykova, Nobuko Yoshida, Romain Demangeon. Practical interruptible conversations: Distributed Dynamic Verification with Session Types and Python. RV 2013: 148-130.
Rumyana Neykova. Session Types Go Dynamic or How to Verify Your Python Conversations.PLACES'13.
Rumyana Neykova, Nobuko Yoshida, Raymond Hu. SPY: Local Verification of Global Protocols. RV 2013: 363-358.
Eduardo R. B. Marques, Francisco Martins, Vasco Thudichum Vasconcelos, Nicholas Ng, Nuno Dias Martins: Towards deductive verification of MPI programs against session types.PLACES'13.
Philip Wadler. Propositions as Sessions. In ICFP 2012.