Effpi: verified message-passing programs in Dotty

Effpi is an experimental toolkit for strongly-typed concurrent and distributed programming in Dotty (a.k.a. the future Scala 3 programming language), with verification capabilities based on type-level model checking.

Resources

This is a temporary website. For now, please refer to the following materials.

Papers

A brief overview of Effpi (4 pages);
A. Scalas, N. Yoshida, E. Benussi. Verifying message-passing programs with dependent behavioural types. PLDI 2019 (to appear). This paper describes the theoretical foundations of Effpi, and evaluates its implementation. Effpi has been reviewed and accepted as companion artifact of the paper.

Implementation

To obtain Effpi's source code (via Git):

git clone https://www.doc.ic.ac.uk/~ascalas/tmp/pldi19/effpi.git

Instructions and requirements: how to build Effpi, its software dependencies, how to reproduce the benchmarks in the PLDI'19 paper, and how to navigate Effpi's source code.
A ready-to-use virtual machine with all Effpi's software dependencies. For details, please read the instructions above.