Tue 25 Jun 2019 08:30 - 08:50 at 224AB - Type Systems I Chair(s): Ranjit Jhala

Concurrent and distributed programming is notoriously hard.
Modern languages and toolkits ease this difficulty by offering
message-passing abstractions, such as actors (e.g., Erlang, Akka,
Orleans) or processes (e.g., Go): they allow for simpler
reasoning w.r.t. shared-memory concurrency, but do not ensure
that a program implements a given specification.

To address this challenge, it would be desirable to \emph{specify
and verify the intended behaviour of message-passing applications
using types}, and ensure that, if a program type-checks and
compiles, then it will run and communicate as desired.

We develop this idea in theory and practice. We formalise a
concurrent functional language $\lambda^{\pi}_{\leq}$, with
a new blend of \emph{behavioural types} (from $\pi$-calculus
theory), and \emph{dependent function types} (from the Dotty
programming language, a.k.a. the future Scala 3). Our theory
yields four main payoffs: (1) it verifies safety and liveness
properties of programs via \emph{type-level model checking}; (2)
unlike previous work, it accurately verifies channel-passing (covering
a typical pattern of actor programs) and higher-order
interaction (i.e., sending/receiving mobile code); (3) it is
directly embedded in Dotty, as a toolkit called Effpi, offering a
simplified actor-based API;
(4) it enables an efficient runtime system for Effpi, for highly
concurrent programs with millions of processes/actors.

Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Type Systems IPLDI Research Papers at 224AB
Chair(s): Ranjit Jhala University of California, San Diego
Verifying Message-Passing Programs with Dependent Behavioural Types
PLDI Research Papers
Alceste Scalas Aston University, Birmingham, UK, Nobuko Yoshida Imperial College London, Elias Benussi Faculty Science Ltd
Toward Efficient Gradual Typing for Structural Types via Coercions
PLDI Research Papers
Andre Kuhlenschmidt Indiana University, Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
Bidirectional Type Checking for Relational Properties
PLDI Research Papers
Ezgi Çiçek Facebook London, Weihao Qu University at Buffalo, SUNY, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
Media Attached