Three papers by members of Computing have been accepted at the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation.

Three papers by members of the Department of Computing have been accepted at the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019), which is a premier forum for programming language research, broadly construed, including
design, implementation, theory, applications, and performance,
to be held in June 24-26, 2019 in Phoenix Arizona, USA.

Imperial's high profile at PLDI 2019 is a nice precursor to PLDI 2020, which will be held in London with Alastair Donaldson from the department serving as General Chair.

Here are details of the papers:

• "Computing Summaries of String Loops in C for Better Testing and Refactoring" by Kapus, Ish-Shalom, Itzhaky, Rinetzky and Cadar is a collaboration between Imperial's Software Reliability Group, Tel Aviv University and Technion. It proposes a novel approach for summarising certain types of string-intensive loops and proves that the summarisation is correct for all input strings. The technique has applications to testing, optimization and refactoring, all of which are explored in the paper. The paper can be accessed at https://srg.doc.ic.ac.uk/publications/19-loops-pldi.html and the associated artifact is available at https://srg.doc.ic.ac.uk/projects/loop-summaries/
• "Sparse Record and Replay with Controlled Scheduling", by Lidbury and Donaldson, introduces a new tool, tsan11rec, that extends the tsan and tsan11 dynamic race detectors to allow controlled scheduling of C++ applications with support for record and replay. Instead of attempting to perform fully-faithful record and reply by instrumenting all system calls, the idea behind tsan11rec is to trade off completeness for efficiency by instrumenting a subset of key system calls on which the nondeterministic behaviour of many popular applications depends. An experimental evaluation comparing the tool with rr, a state-of-the-art record and replay tool, illustrates this trade-off: tsan11rec is more efficient than rr for the record and replay of some applications, but its sparse approach means that it unable to handle applications that the more thorough instrumentation performed by rr enables. Lidbury is a final year PhD student at DoC, supervised by Donaldson. The paper can be accessed at http://multicore.doc.ic.ac.uk/publications/pldi-19.html
• "Verifying Message-Passing Programs with Dependent Behavioural Types" by Scalas, Yoshida and Benussi introduces a novel methodology to implement and verify concurrent and distributed applications in the Dotty programming language (i.e., the future Scala version 3). Its theoretical underpinning is a concurrent functional language with a new blend of behavioural types (from pi-calculus theory), and dependent function types (from Dotty). This approach yields various payoffs: it verifies safety and liveness properties of programs (via type-level model checking); moreover, it naturally leads to an implementation in Dotty: a toolkit called Effpi, offering a simplified actor-based API, and an efficient runtime system for highly concurrent programs with millions of processes/actors. A part of the work was done as Benussi's MEng final year project, which received the Corporate Partnership Programme Award from DoC. The paper is available from http://mrg.doc.ic.ac.uk/publications/verifying-message-passing-programs-with-dependent-behavioural-types/ and the associated peer-reviewed artifact is available from https://www.doc.ic.ac.uk/.ascalas/tmp/pldi19/