Talk: Deadlock and Resource Leak Free Languages

LIVE STREAM: https://uwmadison.zoom.us/j/98728266088?pwd=1kZKc89hFA7oex03np0ZCPSey4Nxp5.1 

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.