Session Types for the Web
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.
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.
As a validation the student can investigate whether existing applications that are heavily based on communication patterns violate this pattern somewhere.
 Pucella, Riccardo, and Jesse A. Tov. "Haskell session types with (almost) no class." ACM Sigplan Notices. Vol. 44. No. 2. ACM, 2008.
 Scalas, Alceste, and Nobuko Yoshida. "Lightweight session types in Scala."
 Munksgaard, Philip, and Thomas Bracht Laumann Jespersen. Practical Session Types in Rust. Diss. Master’s thesis, Department of Computer Science, University of Copenhagen, 2015