Publications
- Formalising Graph Algorithms with Coinduction — January 19, 2025
To appear, at POPL 2025.
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.
Bibtex:
@inproceedings{kidney_formalising_2025, title = {Formalising {{Graph Algorithms}} with {{Coinduction}}}, booktitle = {Proceedings of the 52nd {{Annual ACM SIGPLAN-SIGACT Symposium}} on {{Principles}} of {{Programming Languages}} - {{POPL}} 2025}, author = {Kidney, Donnacha Ois{\'i}n and Wu, Nicolas}, year = {2025}, month = jan, langid = {english} }- Algebraic Effects Meet Hoare Logic in Cubical Agda — January 17, 2024
Presented at POPL 2024.
This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed setoids to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post- conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.
Bibtex:
@inproceedings{kidney_algebraic_2024, title = {Algebraic {{Effects Meet Hoare Logic}} in {{Cubical Agda}}}, booktitle = {Proceedings of the 51st {{Annual ACM SIGPLAN-SIGACT Symposium}} on {{Principles}} of {{Programming Languages}} - {{POPL}} 2024}, author = {Kidney, Donnacha Ois{\'i}n and Yang, Zhixuan and Wu, Nicolas}, year = {2024}, month = jan, publisher = {{ACM Press}}, address = {{Institution of Engineering and Technology (IET), Savoy Place, London}}, abstract = {This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed setoids to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post- conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.}, langid = {english} }- Phases in Software Architecture — August 31, 2023
Presented at FUNARCH 2023.
The large-scale structure of executing a computation can often be thought of as being separated into distinct phases. But the most natural form in which to specify that computation may well have a different and conflicting structure. For example, the computation might consist of gathering data from some locations, processing it, then distributing the results back to the same locations; it may be executed in three phases—gather, process, distribute—but mostly conveniently specified orthogonally—by location. We have recently shown that this multi-phase structure can be expressed as a novel applicative functor (also known as an idiom, or lax monoidal functor). Here we summarize the idea from the perspective of software architecture. At the end, we speculate about applications to choreography and multi-tier architecture.
Bibtex:
@inproceedings{10.1145/3609025.3609479, author = {Gibbons, Jeremy and Kidney, Donnacha Ois\'{\i}n and Schrijvers, Tom and Wu, Nicolas}, title = {Phases in Software Architecture}, year = {2023}, isbn = {9798400702976}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3609025.3609479}, doi = {10.1145/3609025.3609479}, abstract = {The large-scale structure of executing a computation can often be thought of as being separated into distinct phases. But the most natural form in which to specify that computation may well have a different and conflicting structure. For example, the computation might consist of gathering data from some locations, processing it, then distributing the results back to the same locations; it may be executed in three phases—gather, process, distribute—but mostly conveniently specified orthogonally—by location. We have recently shown that this multi-phase structure can be expressed as a novel applicative functor (also known as an idiom, or lax monoidal functor). Here we summarize the idea from the perspective of software architecture. At the end, we speculate about applications to choreography and multi-tier architecture.}, booktitle = {Proceedings of the 1st ACM SIGPLAN International Workshop on Functional Software Architecture}, pages = {29–33}, numpages = {5}, keywords = {phase separation, traversal, applicative functor, fusion, choreography, multi-tier}, location = {Seattle, WA, USA}, series = {FUNARCH 2023} }- Breadth-First Traversal via Staging — September 22, 2022
Presented at MPC 2022 (archive link).
An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird’s `repmin’ problem.
Bibtex:
@InProceedings{10.1007/978-3-031-16912-0_1, author="Gibbons, Jeremy and Kidney, Donnacha Ois{\'i}n and Schrijvers, Tom and Wu, Nicolas", editor="Komendantskaya, Ekaterina", title="Breadth-First Traversal via Staging", booktitle="Mathematics of Program Construction", year="2022", publisher="Springer International Publishing", address="Cham", pages="1--33", abstract="An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define compositionally, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape and contents, traverse the contents, then rebuild the data structure with new contents. We show that this can instead be done directly using staging, expressed using a construction related to free applicative functors. The staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird's `repmin' problem.", isbn="978-3-031-16912-0" }- Algebras for Weighted Search — August 19, 2021
Presented at ICFP 2021.
Weighted search is an essential component of many fundamental and useful algorithms. Despite this, it is relatively under explored as a computational effect, receiving not nearly as much attention as either depth- or breadth-first search. This paper explores the algebraic underpinning of weighted search, and demonstrates how to implement it as a monad transformer. The development first explores breadth-first search, which can be expressed as a polynomial over semirings. These polynomials are generalised to the free semimodule monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad transformer based on the free semimodule monad is introduced. Applying optimisations to this type yields an implementation of pairing heaps, which is then used to implement Dijkstra’s algorithm and efficient probabilistic sampling. The construction is formalised in Cubical Agda and implemented in Haskell.
Bibtex:
@article{10.1145/3473577, author = {Kidney, Donnacha Ois\'{\i}n and Wu, Nicolas}, title = {Algebras for Weighted Search}, year = {2021}, issue_date = {August 2021}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {5}, number = {ICFP}, url = {https://doi.org/10.1145/3473577}, doi = {10.1145/3473577}, abstract = {Weighted search is an essential component of many fundamental and useful algorithms. Despite this, it is relatively under explored as a computational effect, receiving not nearly as much attention as either depth- or breadth-first search. This paper explores the algebraic underpinning of weighted search, and demonstrates how to implement it as a monad transformer. The development first explores breadth-first search, which can be expressed as a polynomial over semirings. These polynomials are generalised to the free semimodule monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad transformer based on the free semimodule monad is introduced. Applying optimisations to this type yields an implementation of pairing heaps, which is then used to implement Dijkstra's algorithm and efficient probabilistic sampling. The construction is formalised in Cubical Agda and implemented in Haskell.}, journal = {Proc. ACM Program. Lang.}, month = {aug}, articleno = {72}, numpages = {30}, keywords = {Haskell, monad, Agda, graph search} }- Finiteness in Cubical Type Theory — September 1, 2020
Master’s thesis.
This thesis will explore and explain finiteness in constructive mathematics: using this setting, it will also serve as an introduction to constructive mathematics in Cubical Agda, and some related topics.
Bibtex:
@phdthesis{kidney_finiteness_2020, title = {Finiteness in {{Cubical Type Theory}}}, author = {Kidney, Donnacha Ois{\'i}n}, year = {2020}, month = sep, address = {{Cork, Ireland}}, url = {https://cora.ucc.ie/handle/10468/11338}, urldate = {2021-05-18}, abstract = {This thesis will explore and explain finiteness in constructive mathematics: using this setting, it will also serve as an introduction to constructive mathematics in Cubical Agda, and some related topics.}, copyright = {https://creativecommons.org/licenses/by-sa/4.0/}, langid = {english}, school = {University College Cork}, annotation = {Accepted: 2021-05-18T09:03:41Z} }- Automatically and Efficiently Illustrating Polynomial Equalities in Agda — April 8, 2019
BSc thesis.
We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda. It is significantly faster than Agda’s existing solver. We use reflection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.
Bibtex:
@phdthesis{kidneyAutomaticallyEfficientlyIllustrating2019, type = {Bachelor Thesis}, title = {Automatically and {{Efficiently Illustrating Polynomial Equalities}} in {{Agda}}}, author = {Kidney, Donnacha Ois{\'i}n}, year = {2019}, month = apr, address = {{Cork, Ireland}}, url = {https://doisinkidney.com/pdfs/bsc-thesis.pdf}, abstract = {We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda. It is signi cantly faster than Agda's existing solver. We use re ection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.}, langid = {english}, school = {University College Cork} }