Reasoning about Equivalence

Speaker: Dr. Jules Jacobs
Cornell University

Title: Reasoning about Equivalence

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:

Equivalence is a fundamental concept in computer science, spanning language and trace equivalences, bisimulation, and semantic or denotational equivalences of programs. In this talk, I will discuss settings where these equivalences can be verified automatically, for instance by deciding program equivalence via language equivalence. We then explore when such verification can be performed efficiently in practice and highlight real-world applications in computer networks.

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.