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.


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

  • Papers
  • 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.


Effpi is developed by:

  • Alceste Scalas — Aston University, Birmingham, UK
  • Elias Benussi — Faculty Science Ltd., UK

The theory behind Effpi is developed in collaboration with:

  • Nobuko Yoshida — Imperial College London, UK