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.
Francesco Tiezzi, Nobuko Yoshida. Reversible Session-Based Pi-Calculus. To appear in JLAMP.
Dimitris Mostrous, Nobuko Yoshida. Session Typing and Asynchronous Subtyping for the Higher-Order Pi-Calculus. Information and Computation.
Nicholas Ng, Jose G.F. Coutinho, Nobuko Yoshida. Protocols by Default: Safe MPI Code Generation based on Session Types. CC 2015.
Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida. Dynamic deadlock verification for general barrier synchronisation. PPoPP 2015.
Julien Lange, Emilio Tuosto, Nobuko Yoshida. From communicating machines to graphical choreographies. POPL 2015.
Dimitrios Kouzapas, Nobuko Yoshida. Globally Governed Session Semantics. LMCS.
Sara Capecchi, Elena Giachino, Nobuko Yoshida. Global Escape in Multiparty Sessions. MSCS.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS.
Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu, Kohei Honda. On Asynchronous Eventful Session Semantics. MSCS.
Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, Nobuko Yoshida. Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python. Formal Methods in System Design.
Dominic Orchard, Nobuko Yoshida. Using session types as an effect system. PLACES 2015.
Dimitrios Kouzapas and Anna Philippou. Type checking privacy policies in the pi-calculus. To appear at FORTE 2015.
Simon Fowler, Loic Denuziere, Adam Granicz. Reactive Single-Page Applications with Dynamic Dataflow. PADL 2015.
Jeremy Siek, Peter Thiemann, Philip Wadler. Blame and Coercion: Together Again for the First Time. To appear at PLDI 2015.
Philip Wadler. Propositions as Types. To appear in Communications of the ACM, 2015.
Philip Wadler. A Complement to Blame. To appear at SNAPL 2015.
Sam Lindley, J. Garrett Morris. A Semantics for Propositions as Sessions. ESOP 2015.
Massimo Bartoletti, Julien Lange, Alceste Scalas, Roberto Zunino. Choreographies in the Wild. Science of Computer Programming.
Laura Bocchi, Weizhen Yang, Nobuko Yoshida. Timed Multiparty Session Types. CONCUR 2014.
Rumyana Neykova, Nobuko Yoshida. Multiparty Session Actors. COORDINATION 2014.
Nicholas Ng, Nobuko Yoshida. Pabble: parameterised Scribble. Service-Oriented Computing and Applications.
Luca Fossati, Raymond Hu, Nobuko Yoshida. Multiparty Session Nets. TGC 2014.
Rumyana Neykova, Laura Bocchi, Nobuko Yoshida. Timed Runtime Monitoring for Multiparty Conversations. BEAT 2014.
Kohei Honda, Nobuko Yoshida, Martin Berger. Process Types as a Descriptive Tool for interaction: Control and the Pi-Calculus. RTA-TLCA 2014.
Kohei Honda, Raymond Hu, Rumyana Neykova, Tzu-Chun Chen, Romain Demangeon, Pierre-Malo Denielou. Structuring Communication with Session Types. COB 2014.
Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. PPDP 2014.
Laura Bocchi, Hernán Melgratti, Emilio Tuosto. Resolving Non-determinism in Choreographics. ESOP 2014.
Søren Debois, Thomas Hildebrandt, Tijs Slatts, Nobuko Yoshida. Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion. FORTE 2014.
Simon J. Gay, Nils Gesbert, Antonio Ravara. Session Types as Generic Process Types. EXPRESS/SOS 2014.
Dimitrios Kouzapas, Ramunas Gutkovas, Simon J. Gay. Session Types for Broadcasting. PLACES 2014.
Giovanni Bernardi, Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas. On Duality Relations for Session Types. TGC 2014.
Ornela Dardha. Recursive Session Types Revisited. BEAT 2014.
Sam Lindley. Algebraic Effects and Effect Handlers for Idioms and Arrows. WGP 2014.
J. Garrett Morris. A Simple Semantics of Haskell Overloading. Haskell 2014.
James Cheney, Sam Lindley, Philip Wadler. Query Shredding: Efficient Relational Evaluation of Queries over Nested Multisets. SIGMOD 2014.
Marco Carbone, Ornela Dardha, Fabrizio Montesi. Progress as Compositional Lock Freedom. COORDINATION 2014.
James Cheney, Sam Lindley, Gabriel Radanne, Philip Wadler. Effective Quotation. PEPM 2014.
Meng Wang and Shayan Najd. Semantic Bidirectionalization Revisited. PEPM 2014.
Sam Lindley, J. Garrett Morris. Sessions as Propositions. PLACES 2014.
Nicholas Ng, Nobuko Yoshida. Pabble: Parameterised Scribble for Parallel Programming. PDP 2014.
Ornela Dardha, Elena Giachino, Michael Lienhardt. A Type System for Components. SEFM 2013.
Nobuko Yoshida, Raymond Hu, Rumyana Neykova, Nicholas Ng. The Scribble Protocol Language. TGC 2013.
Fabrizio Montesi, Nobuko Yoshida. Compositional Choreographies. CONCUR 2013.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 2013.
Dimitrios Kouzapas, Nobuko Yoshida. Globally Governed Session Semantics. CONCUR 2013.
Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, Nobuko Yoshida. Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions. COORDINATION 2013: 45-59.
Ornela Dardha, Daniele Gorla, Daniele Varacca. Semantic Subtyping for Objects and Classes. FORTE/FMOODS 2013.
Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, Nobuko Yoshida. Monitoring Networks through Multiparty Session Types. FORTE/FMOODS 2013.
Pierre-Malo Deniléou, Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. ICALP 2013.
Raymond Hu, Rumyana Neykova, Nobuko Yoshida, Romain Demangeon. Practical interruptible conversations: Distributed Dynamic Verification with Session Types and Python. RV 2013.
Rumyana Neykova. Session Types Go Dynamic or How to Verify Your Python Conversations. PLACES 2013.
Rumyana Neykova, Nobuko Yoshida, Raymond Hu. SPY: Local Verification of Global Protocols. RV 2013.
Eduardo R. B. Marques, Francisco Martins, Vasco Thudichum Vasconcelos, Nicholas Ng, Nuno Dias Martins. Towards Deductive Verification of MPI Programs Against Session Types. PLACES 2013.
Sam Lindley and Conor McBride. Hasochism: the pleasure and pain of dependently typed Haskell programming. Haskell 2013.
James Cheney, Sam Lindley, Philip Wadler. A Practical Theory of Language-Integrated Query. ICFP 2013.
Ohad Kammar, Sam Lindley, Nicolas Oury. Handlers in Action. ICFP 2013.