Paper Info
Title
Verifying message-passing programs with dependent behavioural types
Abstract
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 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 λ≤π, with a new blend of behavioural types (from π-calculus theory), and 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 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.
Year
DOI
Venue
2019
10.1145/3314221.3322484
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
Keywords
Field
DocType
Dotty, Scala, actors, behavioural types, dependent types, model checking, processes, temporal logic
Programming language,Computer science,Theoretical computer science,Message passing
Conference
ISBN
Citations 
PageRank 
978-1-4503-6712-7
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Alceste Scalas1457.06
Nobuko Yoshida262.52
Elias Benussi300.34