A Basis for Concurrency and Distribution


Session types codify the structure of communication, making software more reliable and easier to construct.

From Data Types to Session Types

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 2019.


People


Publications

Available in a combined BibTeX file here.

2017

Sam Lindley, Conor McBride, and Craig McLaughlin. Do be do be do. POPL 2017.

Julien Lange, Nicholas Ng, Bernardo Toninho and Nobuko Yoshida. Fencing off Go: Liveness and Safety for Channel-based Programming. POPL 2017.

Raymond Hu and Nobuko Yoshida. Explicit Connection Actions in Multiparty Session Types. FASE 2017.

Rumyana Neykova and Nobuko Yoshida. Let It Recover: Multiparty Protocol-Induced Recovery. CC 2017.

Julien Lange and Nobuko Yoshida. On the Undecidability of Asynchronous Session Subtyping. FoSSaCS 2017.

2016

O. Dardha, D. Gorla and D. Varacca. Semantic Subtyping for Objects and Classes. The Computer Journal, 2016.

O. Dardha. Type Systems for Distributed Programs: Components and Sessions. Atlantis Press, 2016.

A. L. Voinea and S. J. Gay. Benefits of session types for software development. In: Proceedings of the 7th Workshop on Evaluation and Usability of Programming Languages and Tools -- PLATEAU'16. ACM Press, 2016.

Davide Ancona, Viviana Bono, Mario Bravetti, Giuseppe Castagna, Joana Campos, Simon J. Gay, Elena Giachino, Einar Broch Johnsen, Viviana Mascardi, Nicholas Ng, Luca Padovani, Pierre-Malo Deniélou, Nils Gesbert, Raymond Hu, Francisco Martins, Fabrizio Montesi, Rumyana Neykova, Vasco T. Vasconcelos and Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages 3(2-3):95-230, 2016.

Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages.

Bernardo Toninho, Nobuko Yoshida. Certifying data in multiparty session types. JLAMP.

Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. LMCS.

Rumyana Neykova, Nobuko Yoshida. Multiparty Session Actors. LMCS.

Kohei Honda, Nobuko Yoshida, Marco Carbone. Multiparty Asynchronous Session Types. JACM.

Søren Debois, Thomas Hildebrandt, Tijs Slaats, Nobuko Yoshida. Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion. LMCS.

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. Acta Informatica.

Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida. Characteristic Bisimulations for Higher-Order Session Processes. Acta Informatica.

Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Nobuko Yoshida. Denotational and Operational Preciseness of Subtyping: A Roadmap. Theory and Practice of Formal Methods.

Dimitrios Kouzapas, Ornela Dardha, Roly Perera, Simon J. Gay. Typechecking Protocols with Mungo and StMungo. (Long Version) PPDP 2016.

Sam Lindley, J. Garrett Morris. Embedding Session Types in Haskell. Haskell 2016.

Daniel Hillerström, Sam Lindley. Liberating effects with rows and handlers. TyDe 2016.

Xinyu Niu, Nicholas Ng, Tomofumi Yuki, Shaojun Wang, Nobuko Yoshida, Wayne Luk. EURECA Compilation: Automatic Optimisation of Cycle-Reconfigurable Circuits. FPL 2016.

Roly Perera, Deepak Garg, James Cheney. Causally consistent dynamic slicing. CONCUR 2016.

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler. Coherence generalises duality: a logical explanation of multiparty session types. CONCUR 2016.

Roly Perera, Simon J. Gay. Liveness for Verification. Extended Abstract, LIVE 2016.

Sam Lindley, J. Garrett Morris. Talking Bananas: Structural Recursion for Session Types. ICFP 2016.

J. Garrett Morris. The Best of Both Worlds: Linear Functional Programming Without Compromise. ICFP 2016.

Alceste Scalas, Nobuko Yoshida. Lightweight Session Programming in Scala (with artifact). ECOOP 2016.

Francesco Tiezzi, Nobuko Yoshida. Reversing Single Sessions. RC 2016.

Simon Fowler. An Erlang Implementation of Multiparty Session Actors. ICE 2016.

Roly Perera, Julien Lange, Simon J. Gay. Multiparty Compatibility for Concurrent Objects. PLACES 2016.

Julien Lange, Nobuko Yoshida. Characteristic Formulae for Session Types. TACAS 2016.

Raymond Hu, Nobuko Yoshida. Hybrid Session Verification through Endpoint API Generation. FASE 2016.

Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida. On the Relative Expressiveness of Higher-Order Session Processes. ESOP 2016.

Nicholas Ng, Nobuko Yoshida. Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis. CC 2016.

Bernardo Toninho, Nobuko Yoshida. Certifying Data in Multiparty Session Types. WadlerFest 2016.

Simon Gay. Subtyping Supports Safe Session Substitution. WadlerFest 2016.

Robert Atkey, Sam Lindley, J. Garrett Morris. Conflation Confers Concurrency. WadlerFest 2016.

Shayan Najd, Sam Lindley, Josef Svenningson, Philip Wadler. Everything old is new again: Quoted Domain Specific Languages. PEPM 2016.

Dominic Orchard, Nobuko Yoshida. Effects as sessions, sessions as effects. POPL 2016.

2015

S. J. Gay, N. Gesbert, A. Ravara and V. T. Vasconcelos. Modular Session Types for Objects. Logical Methods in Computer Science 11(4:12), 2015.

O.Dardha. Type Systems for Distributed Programs: Session Communication. In Bulletin of EATCS. Issue of October 2015.

Ornela Dardha, Jorge A. Pérez. Comparing Deadlock-Free Session Typed Processes. EXPRESS/SOS 2015.

Roly Perera, Simon J. Gay. Behavioural Prototypes. Extended Abstract, NOOL 2015.

Hugo A. López, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, Nobuko Yoshida. Protocol-Based Verification of Message-Passing Parallel Programs. OOPSLA 2015.

Michel Steuwer, Christian Fensch, Sam Lindley, Christophe Dubach. Generating Performance Portable Code using Rewrite Rules: From High-level Functional Expressions to High-Performance OpenCL Code. ICFP 2015.

J. Garrett Morris. Variations on Variants. Haskell 2015.

Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida. Characteristic Bisimulations for Higher-Order Session Processes. CONCUR 2015.

Laura Bocchi, Julien Lange, Nobuko Yoshida. Meeting Deadlines Together. CONCUR 2015.

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. CONCUR 2015.

Roly Perera, James Cheney. Proof-Relevant Pi-Calculus. LFMTP 2015.

Francesco Tiezzi, Nobuko Yoshida. Reversible Session-Based Pi-Calculus. 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 verification 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, Anna Philippou. Type checking privacy policies in the pi-calculus. 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. PLDI 2015.

Philip Wadler. Propositions as Types.Communications of the ACM, 2015.

Philip Wadler. A Complement to Blame. SNAPL 2015.

Sam Lindley, J. Garrett Morris. A Semantics for Propositions as Sessions. ESOP 2015.

2014

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 Deniélou. 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, 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.

2013

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, 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.

2012

Ornela Dardha, Elena Giachino, Davide Sangiorgi. Session Types Revisited. PPDP 2012.

Philip Wadler. Propositions as Sessions. ICFP 2012.


Resources

Artifacts

Scribble
Language for describing session types
Mungo
Tools for integrating typestate and session types with Java
Links
Functional language for the web, including session types

Related Research Groups and Projects

BETTY
European project on behavioural typing
MRG
Mobility reading group at Imperial College

ABCD Mailing Lists

abcd-list
General technical discussion relating to ABCD
abcd-interest
Low volume list for anouncements and discussion of ABCD events of interest to everyone involved with ABCD
abcd-work
RAs and PhD students involved with ABCD
abcd-advisory
Advisory board
abcd-scotland
Scottish members of ABCD
abcd-ed
Edinburgh members of ABCD