Deadlock and Resource Leak Free Languages
Jules Jacobs (Cornell University)
Colloquium
Thursday, February 27, 2025, 3:30 pm
Gates Center (CSE2), G20 | Amazon Auditorium
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.
Bio
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.
This talk will be streamed live on our YouTube channel. Link will be available on that page one hour prior to the event.