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

pldi-2019-papers
08:30 - 09:30: PLDI Research Papers - Type Systems I at 224AB
Chair(s): Ranjit JhalaUniversity of California, San Diego
pldi-2019-papers08:30 - 08:50
Talk
Alceste ScalasAston University, Birmingham, UK, Nobuko YoshidaImperial College London, Elias BenussiFaculty Science Ltd
Pre-print
pldi-2019-papers08:50 - 09:10
Talk
Andre KuhlenschmidtIndiana University, Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA
pldi-2019-papers09:10 - 09:30
Talk
Ezgi ÇiçekFacebook London, Weihao QuUniversity at Buffalo, SUNY, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems
Media Attached