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. Lunch and tea/coffee will be provided thanks to funding from VeTSS and the University of Surrey ACE.

Campus Map Register
Registration deadline: 15th July.


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.



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)
A Conflict Free Replicated Tree with Move Operations (short talk) (abstract)

Jean Pichon-Pharabod (University of Cambridge)
Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (short talk) (abstract)
12:30 - 13:30
13:30 - 15:00
Jonathan Lawrence (University of Oxford)
Modelling and Verifying Concurrent Data Types using CSP and FDR (abstract) (slides)

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

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) (slides)

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) (paper)
11:00 - 11:30
Coffee Break
11:30 - 12:30
Jeremy Gibbons (University of Oxford)
What You Needa Know About Yoneda (abstract) (slides)

Alceste Scalas (Aston University)
Effpi: Verified Message-Passing Programs in Dotty (abstract)
12:30 - 13:30
13:30 - 15:00 Dominic Orchard (University of Kent)
Resource-Oriented Programming with Graded Modal Types (abstract) (slides) (GitHub) (project page)

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

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

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) (slides)

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

Aquinas Hobor (National University of Singapore)
Mechanized Verification of Graph-Manipulating Programs (abstract) (slides)