SafeSessions

Full Title

Description

Session types (ST) are nowadays inescapable. Most conferences on programming languages include papers on ST every year, often with a whole session devoted to them. If datatypes describe the structure of data, ST describe the structure of communication in software artifacts. The contribution of types to software quality is well known. Session types add to these a discipline of interaction, setting up the interactive behaviour of the partners involved.
The theory of types in programming languages is by now well established, even if permanently evolving. Witness to that is the number of textbooks on the subject and the courses taught at higher education institutes. That of ST is still in its infancy. There are many dimensions to be discovered, aspects to be systematised, connections to standard type theory to be established.
Session types are linear in the sense that the communication media, usually a channel, has two ends, each of which belongs to a unique thread. Web servers, for example, cannot be linear: one expects a server (or a collection of these) to serve multiple clients. No programming language can rely on linear types alone. But racy (or shared) channels have somewhat been neglected. SafeSessions will study different forms of introducing shared channels in session-based programming languages.
Dependent types allow more precise descriptions of the intended behaviour of software. One can find in the literature a few proposals for the incorporation of dependent types into ST theory, all of which allow types to depend only on shared data. Depending on linear values is technically challenging, but a recent breakthrough, Quantitative Type Theory, opens bright perspectives. SafeSessions will study the incorporation of QTT in the theory of ST, thus allowing for complex behaviours to be captured at type level.
Traditional ST are regular in the sense that types belong to a regular (union omega-regular) language. But there is life beyond regularity. Context-free ST (CFST) allow describing tree-like protocols, enforcing, e.g., that senders correctly stream trees and that receivers correctly receive the tree. But the theory of CFST is still very poor. SafeSessions will study the incorporation of subtyping and higher-order types in CFST.
Types’ natural habitat is programming languages. Despite the relative success of ST, current programming languages do not incorporate ST with the exception of a few prototypes. Session types can be encoded in most programming languages. There are very many such examples in the literature, targetting all conceivable programming languages. Session types in the encoded format are hardly recognised as such: they are verbose, the syntax does not resemble ST at all, shunning its widespread use. The alternative is to adapt existing programming languages. But STs live on top of linear type systems and linearity is not something one may superimpose on a conventional type system. SafeSessions will study the incorporation of ST in mainstream programming languages with support for linearity, paying particular attention to the interplay with other features of the host language, including datatypes, polymorphism, duality, and imperative constructs.
SafeSessions will build compilers for programming languages that further explore the results of the project. Prototypes will be built in the form of plugins for popular IDEs (e.g., Visual Studio Code, Eclipse) or for editors (e.g., Emacs, Atom) that will help programmers with hints as programs are written.
The use of session types is paramount to ensure the correct communication between systems. Robust programming languages designed for the development of applications involving communication is the basis to guarantee correct software. Although the communication between systems is undeniable nowadays, the use of robust languages falls below the needs. The programming language support for developing on top of gRPC or WebSockets, for instance, is close to non-existent. Remote Procedure Calls (RPC) is a concept from the 70s, whose two-way communication structures closely matches session types. gRPC (https://grpc.io) and WebSockets are recent technologies offering fast, bidirectional, communication for web applications. SafeSessions will develop languages to describe protocols and will generate cross-platform client and server bindings for suitable languages.
The team is highly qualified to pursue the objectives of SafeSessions. The PI is one of the proposals of ST. The team has authored many recent papers on topics that SafeSessions will further explore; its members regularly publish at top venues including TCS, I&C, POPL, ICFP, OOPSLA, IJCAI. Furthermore, team members have gathered a large experience in the development of compilers and tools for software development (http://rss.di.fc.ul.pt/tools/sepi/, http://rss.di.fc.ul.pt/tools/confident/, http://rss.di.fc.ul.pt/tools/partypes/, http://rss.di.fc.ul.pt/tools/dol/).

Funding Entity

Reference

DOI

Start Date

End Date

Coordinator

Lines

• Reliable Software Systems

Status