PhD Reading group on Developments in Session Types

Organizers
Marco Carbone
Gian Perrone

Dates of the course: December 2012 - (8 weeks)
The reading group will take place twice per week, with the exact date and time to be decided among the participants. We have proposed Tuesday and Friday, which will be confirmed by the course participants.

Time
Participation: Two hours per meeting (four hours per week)
Preparation: Two hours per meeting (four hours per week).
Three more hours for preparation of a presentation.

Course description
Session types are a modern mechanism for the study, design, and analysis of communicating systems.  The value of type systems has been amply demonstrated in other settings, such that the type safety guarantee provides the assurance “well-typed programs do not go wrong”.  By analogy, session types extend the kinds of behaviours we may describe, such that well-typed programs that engage in communication do not “go wrong”.

The purpose of this course is to gain an insight into the current state of the art in session types, as well as some insight into the areas to which session types may be applied.  We expect the primary focus of the reading group will be to gain a broad understanding, with specific readings directed towards attempting to understand the intersection of theory and practice.  Of the two weekly sessions, the first will be devoted to reviewing older, foundational work in the area to gain a broader understanding, while the second session will be devoted to recent, emerging works.

The format of the course is a reading group, which means that all participants will be expected to read one paper per meeting, and to present at least two papers for discussion during the course.  When reading a paper, participants are expected to reflect upon the reading, integrating and contextualising it with the other readings, and to participate in active discussion.  The format of the presentations will be to give an approximately 30 minute overview of the work, with the remaining one and a half hours devoted to an interactive discussion of the work by all participants.  The presenter for the meeting has the responsibility of directing discussions, and for initiating them by formulating a number of questions for discussion.

Program
The reading group will have an introductory meeting, where the participants discuss and decide the organizational formalities (e.g., meeting times, schedule, etc.). We will discuss the participants’ expectations, further reading proposals and agree on a presentation schedule.

The reading group itself will take place twice per week and will be structured as described above.

After completing the reading list we will have an evaluation meeting with the participants, evaluating if the expectations have been met and if the reading group should continue with new but related contents.

The schedule is premised on the first meetings being held during the first week of December (Tuesday and Friday), and two meetings per week except for the week starting 24^th of December, with the next meeting being held Friday 4^th of January.  The last scheduled meeting will be held on Friday 1^st of February, with possible discussion of whether to continue the reading group in some other format.

Prerequisites
The reading group has not prerequisites. However, it would be advantageous to have some understanding of concepts from concurrency theory, such as exposure to Pi-calculus or some other process calculus.

Exam
The reading group will not have an exam. Students are evaluated by active participation, preparation of two paper presentations, the presentation itself, and by formulating a set of interesting research questions related to their paper presentations, which in turn are used as a foundation for discussion.

Credits
5 ECTS.

Tentative Reading List
The following papers provide a starting point for a reading list.  Depending on the interests of participants, we may amend or substitute these papers in order to focus on a particular area of interest.

• Honda, Kohei, Vasco Vasconcelos, and Makoto Kubo. "Language primitives and type discipline for structured communication-based programming."Programming Languages and Systems (1998): 122-138.
• Dezani-Ciancaglini, Mariangiola, and Ugo De’Liguoro. "Sessions and session types: an overview." Web Services and Formal Methods (2010): 1-28.
• Honda, Kohei, Nobuko Yoshida, and Marco Carbone. "Multiparty asynchronous session types." ACM SIGPLAN NOTICES 43.1 (2008): 273.
• Vallecillo, Antonio, Vasco T. Vasconcelos, and António Ravara. "Typing the behavior of software components using session types." Fundamenta Informaticae 73.4 (2006): 583-598.
• Vasconcelos, Vasco T., Simon J. Gay, and António Ravara. "Type checking a multithreaded functional language with session types." Theoretical Computer Science 368.1 (2006): 64-87.
• Gay, Simon J., et al. "Modular session types for distributed object-oriented programming." ACM Sigplan Notices. Vol. 45. No. 1. ACM, 2010.
• Carbone, Marco, Kohei Honda, and Nobuko Yoshida. "A calculus of global interaction based on session types." Electronic Notes in Theoretical Computer Science 171.3 (2007): 127-151.
• Castagna, Giuseppe, Mariangiola Dezani-Ciancaglini, and Luca Padovani. "On global types and multi-party sessions." Formal Techniques for Distributed Systems (2011): 1-28.
• Carbone, Marco, and Fabrizio Montesi. Typed Multiparty Global Programming⋆. Technical Report, 2011.
• Yoshida, Nobuko, and Vasco T. Vasconcelos. "Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication." Electronic Notes in Theoretical Computer Science 171.4 (2007): 73-93.
• Bonelli, Eduardo, and Adriana Compagnoni. "Multipoint session types for a distributed calculus." Trustworthy Global Computing (2008): 240-256.
• Neubauer, Matthias, and Peter Thiemann. "An implementation of session types." Practical Aspects of Declarative Languages (2004): 56-70.
• Pucella, Riccardo, and Jesse A. Tov. "Haskell session types with (almost) no class." ACM Sigplan Notices. Vol. 44. No. 2. ACM, 2008.
• Gay, Simon. "Bounded polymorphism in session types." Mathematical Structures in Computer Science 18.5 (2008): 895-930.
• Capecchi, Sara, et al. "Session types for access and information flow control."CONCUR 2010-Concurrency Theory (2010): 237-252.