Speakers: Alceste Scalas and Nobuko Yoshida, Imperial College London

Title:  Effpi: concurrent programming with dependent behavioural types

Abstract:
We will first talk about the overview of recent activities in the
Mobility Reading Group at Imperial College London
(http://mrg.doc.ic.ac.uk/).
+ + + + +

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 will talk about Effpi, a toolkit for strongly-typed concurrent
programming in Dotty (a.k.a. Scala 3). 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 (from the pi-calculus theory), and a
form of dependent types, extending to higher-order interaction (i.e.,
concurrent programs with millions of interacting processes/actors.
sending/receiving program thunks). This design has three main
advantages. First, it allows to 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.

Bio:

Nobuko Yoshida is Professor of Computing at Imperial College
London. Last 10 years, her main research interests are theories and
applications of protocols specifications and verifications. She
introduced multiparty session types [ POPL08, JACM ] which received
Most Influential POPL Paper Award in 2018 (judged by its influence
over the last decade). This work enlarged the community and widened
the scope of applications of session types, e.g. runtime monitoring
based on Scribble (co-developed with Red Hat) has been deployed to
other projects such as cyberinfrastructure in the US Ocean
Observatories Initiative(OOI); and widened the scope of her research
areas. She was awarded CNRS and JSSP visiting fellowships and visiting
professorships at Paris VI and Paris VII. She is an editor of ACM
Transactions on Programming Languages and Systems, Mathematical
Structures in Computer Science, Journal of Logical Algebraic Methods
in Programming, and the chief editor of The Computer-aided
Verification and Concurrency Column for EATCS Bulletin. Her current
industry partners include: Cognizant, Estafet, J.P. Morgan, Red Hat,
Weaveworks, November Group, ABB, EDF Energy, Xilinx, EPCC Ltd,
Codeplay Software Ltd and Mexeler.

Alceste Scalas is a Research Associate at Imperial College London,
Dept. of Computing.  Before his PhD, he worked as software developer
in industry, and as research software engineer at CRS4 (Centre for
Advanced Studies, Research and Development in Sardinia).  He is
interested in the theory and practice of concurrent and distributed
systems: how to design and develop correct and reliable applications,
by building upon rigorous mathematical foundations.  His research
topics include concurrency theory, distributed systems, programming
languages, and type systems; he is particularly keen on producing
theoretically-grounded software tools and libraries to aid software
design, development, and verification.