Session Types for the Web

Printer-friendly version
Info
Prerequisites: 
  • Interest in type theory and formal aspects of programming languages
  • Prior knowledge of type theory is a big plus
  • Prior knowledge of JavaScript is recommended but not required
Context: 

The Internet of Things (IoT) is a term for a mass-scale network of devices that share and comsume data. The software that drives these devices is very communication-bounded. If the connection to the outside world is lost, the device can no longer function optimally, or provide one of its features. For example, your internet-connected fridge can still cool your food supplies but it can no longer provide the service of notifying you on your phone if the temperature drops below a certain threshold. 

In this context, the communication part of the program is equally important as the logic of the program. For the logic part of the program there are numerous tools to verify and catch errors before run-time such as a type system.

Session types are a technique that allow the programmer to write down a communication pattern that can be used to verify a protocol at compile-time.  This means that errors against the protocol, such as sending the wrong values, or waiting to receive a value while the server is doing the same thing, can be caught and fixed.

Goal & Research Activities: 

In this thesis the student will investigate how a programmer can specify and check a session type for new and existing programs written in JavaScript and/or TypeScript. Session types have been implemented in Rust [3], Haskell [1] and Scala [2]. To the best of our knowledge this has not yet been done for a web langauge such as JavaScript and/or TypeScript.

Session types have been studied in context of statically strongly typed languages up until now. They have yet to be implemented and studied in context of dynamically typed languages such as JavaScript, where the type checking is mostly done at run-time. This leads to a few problems.  The verification tool can not check if the protocol is respected if it does not know what is being sent on the network.

The first possible approach would be to implement a sort of annotation based mechanism. This means that existing programs can be verified by merely adding annotations to the program text. As a result, existing applications can be verified, as well as new applications. 

The second approach is writing a new small programming language that simply compiles to JavaScript. Both approaches still allow the programmer to write real world applications with verified communication patterns.

As a validation the student can investigate whether existing applications that are heavily based on communication patterns violate this pattern somewhere.

References: 

[1] Pucella, Riccardo, and Jesse A. Tov. "Haskell session types with (almost) no class." ACM Sigplan Notices. Vol. 44. No. 2. ACM, 2008.

[2] Scalas, Alceste, and Nobuko Yoshida. "Lightweight session types in Scala."

[3] Munksgaard, Philip, and Thomas Bracht Laumann Jespersen. Practical Session Types in Rust. Diss. Master’s thesis, Department of Computer Science, University of Copenhagen, 2015