ReactiveSessions is a library for the implementation and specification of communication-based software in the ReactiveML programming language (http://rml.lri.fr/). It borrows inspiration from the FuSe session types implementation (http://www.di.unito.it/~padovani/Software/FuSe/FuSe.html).
This implementation is backed by a published paper: Mauricio Cano, Jaime Arias, Jorge A. Pérez: Session-Based Concurrency, Reactively. FORTE 2017.
All the intuitions about the implementation can be found in the paper. Some of the highlights of our library:
- Correct duality checks for message passing operations.
- Linearity is correctly enforced. This restriction could be relaxed (see below).
- The type of message-passing programs is inferred correctly. There is a caveat to this, see below.
- Adds the possibility of experimenting with reactivity in the models.
Some of the limitations of our prototype, which will be addressed:
- At the moment there is no support for shared channels. This means that linearity is enforced in every channel.
- To properly implement our target session-based pi-calculus, it is necessary to devise a way to encode a blocking output, rather than the current implementation. (ONGOING WORK).
- There is not yet an implementation of the asynchronous pi-calculus presented in the paper. (ONGOING WORK).
- The lack of polymorphic variants in ReactiveML makes it necessary to find a better way to encode selections and branching operators.
To use, simply download or clone the repository and follow the compilation instructions.
- To compile all examples it is only necessary to execute
make. The binaries are copied to the bin folder.
- If you want to clean your project folder, you only need to execute