Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 10:10 - 10:30 at Sala VII - Session 1 Chair(s): Philip Wadler

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.

Slides (beat19-slides.pdf)469KiB

Sun 13 Jan

Displayed time zone: Belfast change

08:30 - 10:30
Session 1BEAT at Sala VII
Chair(s): Philip Wadler University of Edinburgh, UK
08:30
10m
Day opening
Opening
BEAT
António 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
08:40
50m
Talk
Invited Talk: Gradual Session Types — an Ongoing Journey
BEAT
Peter Thiemann University of Freiburg, Germany
09:30
20m
Talk
Gradual Session Types in Imperative Style
BEAT
Kaede Kobayashi Kyoto University, Atsushi Igarashi Kyoto University, Japan
09:50
20m
Talk
Checking the Equivalence of Context-Free Session Types
BEAT
Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
File Attached
10:10
20m
Talk
Effpi: Concurrent Programming with Dependent Behavioural Types
BEAT
Alceste Scalas Imperial College London, Elias Benussi Imperial College London, Nobuko Yoshida Imperial College London
File Attached