一句话：提出以余归纳结构为起点的图与图算法形式化理论，并在 Agda 中实现可复用技术。
图及其算法是计算机科学的基础，但在依赖类型证明助手中形式化尤为困难：图不像树或列表那样是良基的归纳数据类型，标准图算法也常不是结构递归。本文不试图把图改造成普通归纳类型，而是从一开始就把图视为余归纳结构，建立图与图算法的形式理论，并在 Agda 中实现。该路线面临 Agda 更擅长归纳而非余归纳、且形式化依赖商类型（quotient types）而商类型会进一步增加余归纳处理难度等挑战。作者发展出可复用技术来应对这些问题；其核心的简洁图表示被证明灵活、强大且可形式化。
Graphs and their algorithms are fundamental to computer science, but they can be difficult to formalise, especially in dependently-typed proof assistants. Part of the problem is that graphs aren’t as well-behaved as inductive data types like trees or lists; another problem is that graph algorithms (at least in standard presentations) often aren’t structurally recursive. Instead of trying to find a way to make graphs behave like other familiar inductive types, this paper builds a formal theory of graphs and their algorithms where graphs are treated as coinductive structures from the beginning. We formalise our theory in Agda. This approach has its own unique challenges: Agda is more comfortable with induction than coinduction. Additionally, our formalisation relies on quotient types, which tend to make coinduction even harder to deal with. Nonetheless, we develop reusable techniques to deal with these difficulties, and the simple graph representation at the heart of our work turns out to be flexible, powerful, and formalisable.