Formalising Graph Algorithms with Coinduction

This conference talk from POPL 2025 explores a novel approach to formalizing graph algorithms using coinduction. Presented by Donnacha Oisín Kidney and Nicolas Wu from Imperial College London, the 21-minute presentation addresses the challenges of formalizing graphs in dependently-typed proof assistants. Rather than forcing graphs to behave like inductive data types, the speakers demonstrate how treating graphs as coinductive structures from the beginning creates a more natural formalization. Learn about their implementation in Agda, including how they overcome challenges related to quotient types and coinduction. The presentation showcases reusable techniques that make their graph representation flexible, powerful, and formally verifiable. The research contributes to the fields of Cubical Agda, coinduction, graphs, and algebraic graph theory, offering valuable insights for those working with formal verification of graph algorithms.