Tuesday, 1 April 2025, London

VeTSS supported the 16th edition of S-REPLS, which took place at Imperial College London on 1st April 2025, and was a big success! With more than 100 attendees from all around the country, the programme opened with a keynote from Sophia Drossopoulou (Imperial) and Matthew Parkinson (Azure Research, Microsoft) about behaviour-oriented concurrency, its adoption in Project Verona, and the use of behaviour-oriented concurrency ideas in bringing concurrency to Python in a principled manner.

The rest of the morning featured contributed talks from academia and industry: Jake Hughes (King’s College London) spoke about work on garbage collection for Rust, Oliver Pearce (Royal Holloway, University of London), presented recent work on stateless model checking for Rust, and Akos Hajdu (Meta) talked about the use of call graph reachability for reasoning about the WhatsApp android app.

After an excellent lunch provided by local firm Jakobs (with costs covered by VeTSS), the afternoon focused on program logics and type systems, with talks from Andreas Loow (Imperial) on compositional symbolic execution, Rao Xiaojia (Imperial) on WebAssembly mechanisation, Benedict Bunting (Oxford) on reachability types, traces and full abstraction, and Yulong Huang (Cambridge) on substitution, normalization and formalization.

The event concluded with a talk from Andy Gordon (Cogna) on the use of AI techniques to generate formal specifications for software and explain them to end users, after which discussions continued over enjoyable drinks at Imperial’s Eastside bar.

Abstracts for all of the talks are available on the S-REPLS 16 website.

By Alastair Donaldson