SPLV 2021

This year, the Scottish Programming Languages and Verification Summer School returns to Glasgow (at least, virtually). The online event is organized by the School of Computing Science at the University of Glasgow[University of Glasgow tower].

SPLV 2021 is scheduled across two consecutive weeks: Monday 9 August – Friday 13 August, then Monday 16 August – Wednesday 18 August, with 1-2 hours commitment most days.  Lectures will run live via Zoom, with follow-up Q+A facilitated on the SPLV Slack and/or SPLS Zulip. Participation is free since the event is entirely virtual. Please register for SPLV participation by completing this registration form.


Simon Peyton Jones (Microsoft Research) –  Hashing Modulo Alpha Equivalence

[Simon Peyton Jones headshot]

photo CC BY-SA 4.0
(based on original version by Duncan.Hull)

In many applications, one wants to identify identical subtrees of a program syntax tree. This identification should ideally be robust to alpha-renaming of the program, but no existing technique has been shown to achieve this with good efficiency (better than O(n^2) in expression size). We present a new, asymptotically efficient way to hash modulo alpha-equivalence. A key insight of our method is to use a weak (commutative) hash combiner at exactly one point in the construction, which admits an algorithm with O(n*(log n)^2) time complexity. We prove that the use of the commutative combiner nevertheless yields a strong hash with low collision probability.

Guy Katz (Hebrew University of Jerusalem) – [Guy Katz]Safety in AI Systems: SMT-Based Verification of Neural Networks

Guy’s research focuses on applying formal methods to enable the creation of reliable and correct software. He is particularly interested in formally verifying systems that feature machine-learned components, such as neural networks. For instance, the Marabou framework for verifying deep neural networks is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into constraint satisfaction problems.

Jennifer Allanson (Tuplespace) – How to present your research online[Jen Allanson]

The world has changed. Online networking and relationship building has become an important part of professional academic practice. Presenting your work online in a manner which is engaging and informative will create valuable opportunities. In this workshop we will think about different audiences for our work, identify ways to make what we do interesting to people with different backgrounds and specialisms, and think about how to create and tell memorable stories about our work, considering ways to encourage interactivity and question asking.

Ilyena Hirskyj-Douglas (University of Glasgow) – [Ilyena Hirskyj-Douglas]Stories of Programming Computers for Animals

In this talk, Ilyena Hirskyj-Douglas will go over examples of novel systems she has created for dogs and monkeys, telling stories of both failures and successes, also speculating on the future of computer systems for animals.

Provisional Schedule

All times are UK BST (UTC+1)

Mon 9 Aug, 1000-1130 Guy Katz (Safety in AI Systems – part 1)
Mon 9 Aug, 1400-1530 Simon Peyton Jones (Hashing Modulo Alpha Equivalence)
Tue 10 Aug, 1000-1130 Guy Katz (Safety in AI Systems – part 2)
Wed 11 Aug, 1000-1130 Guy Katz (Safety in AI Systems – part 3)
Thu 12 Aug, 1000-1130 Guy Katz (Safety in AI Systems – part 4)
Fri 13 Aug, 1000-1200 Jennifer Allanson (How to present your research online)
Fri 13 Aug, 1400-1530 Virtual expedition (details to follow)
Mon 16 Aug, 1000-1130 1400-1530 Ilyena Hirskyj-Douglas (Programming Computers for Animals)
Tue 17 Aug, 1400-1530 Virtual poster session 1
Wed 18 Aug, 1400-1530 Virtual poster session 2


SPLV 2021 is being organized by:


SPLV 2021 is kindly sponsored by the Scottish Informatics and Computer Science Alliance.

[SICSA logo]