Effpi: Concurrent Programming with Dependent Behavioural Types
This is a report of ongoing work
Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.
We address this challenge with Effpi: a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. the future Scala 3 programming language). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.
The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving mobile code). This design has three main advantages. First, it allows to statically verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes / actors.
Sun 13 JanDisplayed time zone: Belfast change
08:30 - 10:30
Session 1BEAT at Sala VII
Chair(s): Philip Wadler University of Edinburgh, UK
Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. Pérez University of Groningen, The Netherlands
|Invited Talk: Gradual Session Types — an Ongoing Journey|
Peter Thiemann University of Freiburg, Germany
|Gradual Session Types in Imperative Style|
Kaede Kobayashi Kyoto University, Atsushi Igarashi Kyoto University, Japan
|Checking the Equivalence of Context-Free Session Types|
Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of LisbonFile Attached
|Effpi: Concurrent Programming with Dependent Behavioural Types|
Alceste Scalas Imperial College London, Elias Benussi Imperial College London, Nobuko Yoshida Imperial College LondonFile Attached