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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

08:30 - 10:30: Session 1BEAT at Sala VII
Chair(s): Philip WadlerUniversity of Edinburgh, UK
08:30 - 08:40
Day opening
Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. PérezUniversity of Groningen, The Netherlands
08:40 - 09:30
Invited Talk: Gradual Session Types — an Ongoing Journey
Peter ThiemannUniversity of Freiburg, Germany
09:30 - 09:50
Gradual Session Types in Imperative Style
Kaede KobayashiKyoto University, Atsushi IgarashiKyoto University, Japan
09:50 - 10:10
Checking the Equivalence of Context-Free Session Types
Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon
File Attached
10:10 - 10:30
Effpi: Concurrent Programming with Dependent Behavioural Types
Alceste ScalasImperial College London, Elias BenussiImperial College London, Nobuko YoshidaImperial College London
File Attached