Deadlock and Resource Leak Free Languages

Speaker: Dr. Jules Jacobs
Cornell University

Title: Deadlock and Resource Leak Free Languages

Date: Monday, 31 March 2025

Time: 4:00pm - 5:00pm

Venue: Lecture Theater F
(Leung Yat Sing Lecture Theater), near lift 25/26, HKUST

Abstract:

Reasoning about concurrent programs is notoriously difficult, especially when multiple threads share data. While concurrency primitives such as message-passing channels and locks help synchronize access to shared resources, their misuse can still lead to deadlocks and resource leaks—even in memory-safe languages like Go and Rust. Contrary to popular belief, Rust’s type system does not fully prevent these issues. This talk explores programming language and type system designs that do statically guarantee that well-typed programs are both deadlock-free and resource leak-free, eliminating these pitfalls by construction.

Biography:

Jules Jacobs is a computer science researcher working on programming languages, formal methods, and concurrency. He completed his PhD at Radboud University and is currently a postdoctoral researcher at Cornell University. His work includes deadlock- and leak-free type systems, concurrent separation logic for message passing, probabilistic programming, and automata-based verification of networking policies.