Surrey Concurrency Workshop and S-REPLS 12

University of Surrey, Guildford

23‐24 July, 2019

This two-day workshop is aimed at bringing together researchers, from the UK and elsewhere, who are working on the theory of concurrency and the semantics and implementation of programming languages.

The workshop will be held in Lecture Theatre L of the LT building (see Campus Map). Directions to the Stag Hill Campus are available here.

Registration for the event is free thanks to funding from VeTSS and the University of Surrey ACE.

Campus Map Propose talk Register
Registration deadline: 5th July.
There is still time to propose talks. Please e-mail suggestions to


Further announcements about the workshop will be made via the Concurrency Working Group and S-REPLS mailing lists. Please subscribe by following those links and clicking Subscribe or Unsubscribe.


Brijesh Dongol

Concurrency Workshop Steering Committee
Mark Batty, Mike Dodds, Philippa Gardner, Cliff Jones and Matthew Parkinson
S-REPLS Steering Committee
Dominic Mulligan, Ohad Kammar and Jeremy Yallop


Participants may wish to stay in nearby hotels or on campus. However, it is also possible to commute from London. Guildford is approx 35 mins by train from London Waterloo, and the University is a 15 min walk from Guildford station.

Some possible hotel options are below. These are approx a 25-30 min walk to campus.

Draft Schedule

Date Time Event
9:30 - 10:00
Coffee and Refreshments
10:00 - 10:05
10:05 - 11:00
Invited Talk
Gregory Chockler (Royal Holloway)
Atomic Transaction Commit for Modern Data Stores (abstract)
11:00 - 11:30
Coffee Break
11:30 - 12:30
Shale Xiong (Imperial College London)
Data Consistency in Transactional Storage Systems: A Centralised Approach (abstract)

Victor Gomes (University of Cambridge)
TBD (abstract)
12:30 - 13:30
13:30 - 15:00
Jonathan Lawrence (University of Oxford)
Modelling and Verifying Concurrent Lock Free Data Types using CSP and FDR (abstract)

Ioana Boureanu (University of Surrey)
Symbolic Verification of Epistemic Properties in Programs (abstract)

Emanuele D'Osualdo (Imperial College London)
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs (abstract)
15:00 - 15:30
Coffee Break
15:30 - 17:00
Gustavo Petri (ARM, Cambridge)
Proving Invariant Safety of Highly Available Distributed Applications (abstract)

Conrad Watt and Guillaume Barbier (University of Cambridge)
Mending JavaScript's Relaxed Memory Model (abstract)

Alasdair Armstrong (University of Cambridge)
Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Sail (abstract)
Date Time Event
9:30 - 10:00
Coffee and Refreshments
10:00 - 11:00
Invited Talk
Ornela Dardha (University of Glasgow)
A New Linear Logic for Deadlock-Free Session-Typed Processes (abstract)
11:00 - 11:30
Coffee Break
11:30 - 12:30
Jeremy Gibbons (University of Oxford)
What You Needa Know About Yoneda (abstract)

Alceste Scalas (Aston University)
Effpi: Verified Message-Passing Programs in Dotty (abstract)
12:30 - 13:30
13:30 - 15:00 Vilem Liepelt (University of Kent)
Resource-Oriented Programming with Graded Modal Types (abstract)

James Noble (Victoria University of Wellington)
Transient Typechecks are (Almost) Free (abstract)

Francois Dupressoir (University of Surrey)
EasyCrypt: Applying Program Verification Techniques to Cryptography (abstract)
15:00 - 15:30
Coffee Break
15:30 - 17:00

Marco Paviotti (University of Kent)
First Steps in Denotational Semantics for Weak Memory Concurrency (abstract)

Evgenii Moiseenko (JetBrains Research)
Compilation Correctness from Event Structure Based Weak Memory Model (abstract)

Simon Doherty (University of Sheffield)
Local Data-Race Freedom and the C11 Memory Model (abstract)