{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T05:47:17Z","timestamp":1784180837172,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>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\u2019t as well-behaved as inductive data types like trees or lists; another problem is that graph algorithms (at least in standard presentations) often aren\u2019t 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.<\/jats:p>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1145\/3704892","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1657-1686","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalising Graph Algorithms with Coinduction"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4952-7359","authenticated-orcid":false,"given":"Donnacha Ois\u00edn","family":"Kidney","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00728-4"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TLCA.2015.17"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01182254"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_8_1","volume-title":"Closure Algorithms and the Star-Height Problem of Regular Languages","author":"Backhouse Roland","year":"1975","unstructured":"Roland Backhouse. 1975. Closure Algorithms and the Star-Height Problem of Regular Languages. Ph. D. Dissertation. Imperial College London. https:\/\/cir.nii.ac.jp\/crid\/1570854175242787968"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/imamat\/15.2.161"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)90005-1"},{"issue":"2","key":"e_1_3_2_11_1","article-title":"Guarded Cubical Type Theory: Path Equality for Guarded Recursion","volume":"50","author":"Birkedal Lars","year":"2016","unstructured":"Lars Birkedal, Ale\u0161 Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2016. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Vol. 50. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2. arXiv:1606.05223 http:\/\/arxiv.org\/abs\/1606.05223","journal-title":"25th EACSL Annual Conference on Computer Science Logic (CSL 2016)"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000184"},{"key":"e_1_3_2_13_1","volume-title":"Regular Algebra and Finite Machines","author":"Conway John Horton","year":"1971","unstructured":"John Horton Conway. 1971. Regular Algebra and Finite Machines. Chapman and Hall, London."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500613"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90024-7"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004075"},{"key":"e_1_3_2_17_1","unstructured":"Martin Erwig. 2008. Functional Graph Library\/Haskell. https:\/\/web.engr.oregonstate.edu\/~erwig\/fgl\/haskell\/"},{"key":"e_1_3_2_18_1","unstructured":"David Feuer. 2022. Containers: Assorted Concrete Container Types. Haskell. https:\/\/hackage.haskell.org\/package\/containers"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.207.4"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01840439"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_16"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003912"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60117-1_16"},{"key":"e_1_3_2_24_1","unstructured":"Jeremy Gibbons and Graham Hutton. 1999. Proof Methods for Structured Corecursive Programs. In Proceedings of 1st Scottish Workshop on Functional Programming."},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632869"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_16"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.20"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473577"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199530"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2024\/8\/9"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Jade Master. 2021. The Open Algebraic Path Problem. https:\/\/doi.org\/10.48550\/arXiv.2005.06682 10.48550\/arXiv.2005.06682 arXiv:2005.06682","DOI":"10.48550\/arXiv.2005.06682"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Jade Master. 2022. How to Compose Shortest Paths. https:\/\/doi.org\/10.48550\/arXiv.2205.15306 10.48550\/arXiv.2205.15306 arXiv:2205.15306","DOI":"10.48550\/arXiv.2205.15306"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.05.003"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122956"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2022\/6\/12"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-349-91518-7_10"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.39.649"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790514"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_27"},{"key":"e_1_3_2_42_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100846"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704892","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704892","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:35Z","timestamp":1770200135000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704892"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704892"],"URL":"https:\/\/doi.org\/10.1145\/3704892","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}