Preface

This volume contains the proceedings of PLACES 2017, the 10th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The workshop was held in Uppsala, Sweden, on April 29th 2017, co-located with ETAPS, the European Joint Conferences on Theory and Practice of Software. The PLACES workshop series aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future: the development of programming languages, methodologies, and infrastructures where concurrency and distribution are the norm rather than a marginal concern. Previous editions of PLACES were held in Eindhoven (2016), London (2015), Grenoble (2014), Rome (2013), Tallin (2012), Saarbrücken (2011), Paphos (2010) and York (2009), all co-located with ETAPS, and the first PLACES was held in Oslo and co-located with DisCoTec (2008).

The Program Committee of PLACES 2017 consisted of:

• Sebastian Burckhardt, Microsoft Research, USA
• Ilaria Castellani, INRIA Sophia Antipolis, FR
• Marco Carbone, IT University of Copenhagen, DK
• Silvia Crafa, University of Padua, IT
• Patrick Eugster, TU Darmstadt, DE
• Ganesh L. Gopalakrishnan, University of Utah, USA
• Philipp Haller, KTH Royal Institute of Technology, SE (co-chair)
• Dimitrios Kouzapas, University of Glasgow, UK
• Sam Lindley, University of Edinburgh, UK
• Luca Padovani, University of Turin, IT
• Aleksandar Prokopec, Oracle Labs, CH
• Peter Thiemann, University of Freiburg, DE
• Vasco T. Vasconcelos, University of Lisbon, PT (co-chair)

The Program Committee, after a careful and thorough reviewing process, selected 8 papers out of 9 submissions for presentation at the workshop. Each submission was evaluated by at least three referees, and the accepted papers were selected during a week-long electronic discussion. Revised versions of all the accepted papers appear in these proceedings.

In addition to the contributed papers, the workshop featured two invited talks: first, a talk by Dave Clarke, Uppsala University, entitled The Encore Programming Language: Actors, Capabilities, Garbage, ...; second, a talk by Edwin Brady, University of St Andrews, entitled Dependent Types for Correct Concurrent Programming.

PLACES 2017 was made possible by the contribution and dedication of many people. We thank all the authors who submitted papers for consideration. Thanks also to our invited speakers, Dave Clarke and Edwin Brady. We are extremely grateful to the members of the Program Committee and additional experts for their careful reviews, and the balanced discussions during the selection process. The EasyChair system was instrumental in supporting the submission and review process; the EPTCS website was similarly useful in production of these proceedings.

March 30th, 2017
Vasco T. Vasconcelos
Philipp Haller

The Encore Programming Language: Actors, Capabilities, Garbage, ... (Invited Talk)

Encore is an actor-based programming language developed in the context of the FP7 EU Project UPSCALE. Encore is aimed at general purpose parallel programming, and shuns multithreading to avoid the lack of scalability associated with it. Encore shares a run-time with the pure actor language Pony, which, in contrast to more common run-times, offers local, per-actor garbage collection. Encore includes various abstractions for parallelism and concurrency whose correct behaviour depends, surprisingly, on correct interaction with the garbage collector. To facilitate correct behaviour and allow safe communication between actors, Encore offers a novel capability language. This talk will describe Encore, how it uses and abuses the Pony run-time, the garbage-collection related problems that ensue, and the capability language that resolves them.

Dependent Types for Correct Concurrent Programming (Invited Talk)

Modern software systems rely on communication, for example mobile applications communicating with a central server, distributed systems coordinating a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent programs is hard, since we must reason about each process and the order in which communication might happen between processes. In this talk, I will describe an approach to implementing communicating concurrent programs, inspired by Session Types, using the dependently typed programming language Idris.

I will introduce Idris, and show how its type system can be used to describe resource access protocols (such as controlling access to a file handle or managing the state transitions for logging in to a secure data store) and verify that programs correctly follow those protocols. I will then show how to use this type-driven approach to resource tracking to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.

By type-driven, I mean that the approach involves writing an explicit type describing the pattern of communication, and verifying that processes follow that pattern by type-checking. Communication channels are explicitly parameterised by their state; operations on a channel require a channel in the correct state, and update the channel's state. As a result, a well-typed program working with a communication channel is guaranteed to follow the correct protocol for that channel.