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


People

Alumni

Advisory Board

  • Matthew Arrott (November Group)
  • Andrew Birkett (Amazon)
  • Gary Brown (Redhat)
  • Mariangiola Dezani (University of Torino)
  • Bippin Makoond (Cognizant)
  • Frank Pfenning (Carnegie Mellon University)
  • Alexis Richardson (Weaveworks)
  • Steve Ross-Talbot (Estafet)
  • Vasco Vasconselos (University of Lisbon)

Publications

Available in a combined BibTeX file here.

2020

A. Laura Voinea, Ornela Dardha, Simon J. Gay. Typechecking Java Protocols with [St]Mungo. FORTE, 2020.

Artem Usov, Ornela Dardha. SFJ: An Implementation of Semantic Featherweight Java. COORDINATION, 2020.

2019

Simon Castellan, Nobuko Yoshida. Two Sides of the Same Coin: Session Types and Game Semantics. POPL 2019.

David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, Nobuko Yoshida. Distributed Programming Using Role Parametric Session Types in Go. POPL 2019.

Tiago Cogumbreiro, Raymond Hu, Francisco Martins, and Nobuko Yoshida. Dynamic Deadlock Verification for General Barrier Synchronisation. TOPLAS 2019.

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Journal of Functional Programming, 29(e15), 2017.

Simon Fowler, Sam Lindley, J. Garrett Morris, Sára Decova. Exceptional Asynchronous Session Types: Session Types without Tiers. POPL 2019.

Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. Journal of Logic and Algebraic Methods in Programming, vol. 104, 2019.

Eva Graversen, Iain Phillips, Nobuko Yoshida. Towards a Categorical Representation of Reversible Event Structure. Journal of Logical and Algebraic Methods in Programming, vol. 104, 2019.

Keigo Imai, Nobuko Yoshida, Shoji Yuen. Session-ocaml: a Session-based Library with Polarities and Lenses. Science of Computer Programming, 2019.

Wen Kokke. Rusy Variation: Deadlock-free Sessions with Failure in Rust. ICE, 2019.

Wen Kokke, Fabrizio Montesi, Marco Peressotti. Better Late than Never: A Fully Abstract Semantics for Classical Processes. POPL 2019.

Wen Kokke, J. Garrett Morris, and Philip Wadler. Towards Races in Linear Logic. COORDINATION, 2019.

Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida. On the Relative Expressiveness of Higher-Order Session Processes. Information and Computation, vol. 268, 2019.

J. Garrett Morris and James McKinna. Abstracting Extensible Data Types: Or, Rows by Any Other Name. POPL 2019.

Alceste Scalas, Nobuko Yoshida. Less Is More: Multiparty Session Types Revisited. POPL 2019.

Tom Schrijvers, Bruno C.D.S. Oliveira, Philip Wadler, and Koar Marntirosian. COCHIS: Stable and coherent implicits Journal of Functional Programming, 29(e3), 2019.

Bernardo Toninho, Nobuko Yoshida. Interconnectability of Session Based Logical Processes. TOPLAS, 2019.

A. Laura Voinea, Ornela Dardha, Simon J. Gay. Resource Sharing via Capability-Based Multiparty Session Types. IFM, 2019.

2018

Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida. Dynamic deadlock verification for general barrier synchronisation. TOPLAS, 2018.

Wen Kokke, Fabrizio Montesi, Marco Peressotti. Taking Linear Logic Apart. Linearity/TLLA 2018.

Philip Wadler. Programming Language Foundations in Agda. SMBF 2018.

Philip Wadler and Wen Kokke. Programming Language Foundations in Agda. Online book.

Jack Williams, J. Garrett Morris, Philip Wadler. The Root Cause of Blame: Contracts for Intersection and Union Types. OOPSLA 2018.

Daniel Hillerström and Sam Lindley. Shallow Effect Handlers. APLAS 2018.

Roly Perera, James Cheney. Proof-relevant pi-calculus: a constructive account of concurrency and causality. Mathematical Structures in Computer Science 28(9):1541-1577, 2018.

Rudi Horn, Roly Perera, James Cheney. Incremental relational lenses. Proceedings of the ACM on Programming Languages 2(ICFP) 74:1-74:30, 2018.

Ebrahim Ardeshir-Larijani, Simon Gay, Rajagopal Nagarajan. Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic 19(4) 28:1-28:32, 2018.

Doriana Medic, Claudio Antares Mezzina, Iain Phillips, Nobuko Yoshida. A Parametric Framework for Reversible Pi-Calculi. EXPRESS/SOS'18.

Rumyana Neykova, Raymond Hu, Nobuko Yoshida, Fahd Abdeljallal. A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#. CC 2018.

Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, Lukasz Ziarek. A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. ESOP 2018.

Romain Demangeon, Nobuko Yoshida. Causal Computational Complexity of Distributed Processes. LICS 2018.

Bernardo Toninho, Nobuko Yoshida. Depending On Session Typed Process. FoSSaCS 2018.

Eva Graversen, Iain Phillips, Nobuko Yoshida. Event Structure Semantics of (controlled) Reversible CCS. RC 2018

Alceste Scalas, Nobuko Yoshida. Multiparty Session Types, Beyond Duality. JLAMP.

Bernardo Toninho, Nobuko Yoshida. On Polymorphic Sessions And Functions: A Tale of Two (Fully Abstract) Encodings. ESOP 2018.

Ornela Dardha, Simon J. Gay. A New Linear Logic for Deadlock-Free Session Typed Processes. FoSSaCS 2018.

Dimitrios Kouzapas, Ornela Dardha, Roly Perera, Simon J. Gay. Typechecking protocols with Mungo and StMungo: A session type toolchain for Java. Sci. Comput. Program. 155: 52-75, 2018.

Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala. Refinement Reflection: Complete Verification with SMT. POPL 2018.

Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida. A Static Verification Framework for Message Passing in Go using Behavioural Types. ICSE 2018.

2017

Philip Wadler. Abstract Data Types without the Types. Journal of Universal Computer Science, 2017.

Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler. Quantified Class Constraints.. Haskell 2017.

Alceste Scalas, Nobuko Yoshida. Multiparty Session Types, Beyond Duality. PLACES 2017.

Eva Graversen, Iain Phillips, Nobuko Yoshida. Towards a Categorical Representation of Reversible Event Structure. PLACES 2017.

Simon Castellan. Concurrent Structures in Game Semantics. The Concurrency Column, EATCS Bulletin.

Simon J. Gay, Antonio Ravara (editors). Behavioural Types: from Theory to Tools. River Publishers, 2017.

Ornela Dardha, Elena Giachino, Davide Sangiorgi. Session Types Revisited. Inf. Comput. 256: 253-286, 2017.

Ornela Dardha, Daniele Gorla, Daniele Varacca. Semantic Subtyping for Objects and Classes. Comput. J. 60(5): 636-656, 2017.

Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas, Roly Perera, Adriana L. Voinea, Florian Weber. Mungo and StMungo: Tools for Typechecking Protocols in Java. Behavioural Types: from Theory to Tools. River publishers, 2017.

Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney. Imperative Functional Programs That Explain Their Work. ICFP 2017.

Roly Perera, James Cheney. Proof-Relevant π-Calculus: A Constructive Account of Concurrency and Causality. Mathematical Structures in Computer Science, 2017.

Weili Fu, Roly Perera, Paul Anderson, James Cheney. muPuppet: A Declarative Subset of the Puppet Configuration Language. ECOOP 2017.

Rumyana Neykova and Nobuko Yoshida. How to Verify Your Python Conversations. Behavioural Types: from Theory to Tools. River publishers, 2017.

Julien Lange, Emilio Tuosto, and Nobuko Yoshida. A Tool for Choreography-Based Analysis of Message-Passing Software. Behavioural Types: from Theory to Tools. River publishers, 2017.

Dominic Orchard and Nobuko Yoshida. Session Types with Linearity in Haskell. Behavioural Types: from Theory to Tools. River publishers, 2017.

Raymond Hu. Distributed Programming Using Java APIs Generated from Session Types. Behavioural Types: from Theory to Tools. River publishers, 2017.

Nicholas Ng and Nobuko Yoshida. Protocol-Driven MPI Program Generation. Behavioural Types: from Theory to Tools. River publishers, 2017.

Vasco T. Vasconcelos, Francisco Martins, Eduardo R.B. Marques, Nobuko Yoshida, and Nicholas Ng. Deductive Verification of MPI Protocols. Behavioural Types: from Theory to Tools. River publishers, 2017.

Daniel Hillerström, Sam Lindley, Robert Atkey, and KC Sivaramakrishnan. Continuation passing style for effect handlers. FSCD 2017.

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. ICFP 2017.

J. Garrett Morris and Richard A. Eisenberg. Constrained Type Families. ICFP 2017.

Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. Gradual Session Types ICFP 2017.

Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for Free for Free: Parametricity, With and Without Types ICFP 2017.

Bernardo Toninho and Nobuko Yoshida. Certifying data in multiparty session types. Journal of Logical and Algebraic Methods in Programming, vol. 90, August 2017.

Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, vol. 13, issue 2, 2017.

Simon Fowler, Sam Lindley, Philip Wadler. Mixing Metaphors: Actors as Channels and Channels as Actors. ECOOP 2017.

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. ECOOP 2017.

Sam Lindley and J. Garrett Morris. Lightweight functional session types. In: Behavioural Types: from Theory to Tools. River publishers, 2017.

Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. ECOOP 2017.

Keigo Imai, Nobuko Yoshida, and Shoji Yuen. Session-ocaml: a session-based library with polarities and lenses. COORDINATION 2017.

Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring Networks through Multiparty Session Types. Theoretical Computer Science, vol. 669, March 2017.

Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed Runtime Monitoring for Multiparty Conversations. Formal Aspects of Computing, vol. 29, issue 5, 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.

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

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

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

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.

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.

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, Concurrency Column. 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, and tool for generating type-safe session APIs in Java and Scala
Mungo
Tools for integrating typestate and session types with Java
Links
Functional language for the web, including session types
lchannels
A library for type-safe session programming in Scala
Session-ocaml
A session types library for OCaml

Related Research Groups and Projects

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