Donnacha Oisín Kidney
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- POPL3 editions2024–2026
on a stage with
all 4 in the filters
who talks about the same things
- Zhixuan Yang3 talks
- Nicolas Wu25 talks
- Henning Urbat6 talks
- Ugo Dal Lago14 talks
- Ohad Kammar19 talks
- Sharon Shoham13 talks
| title | conference | date |
|---|---|---|
| Hyperfunctions: Communicating Continuations | POPL 2026 | 2026-01-11 |
Identifies a recurring type — the hyperfunction — that actually implements communication between continuations and concurrent processes, shows it appears in… | ||
| Formalising Graph Algorithms with Coinduction | POPL 2025 | 2025-01-19 |
Formalisation in Cubical Agda treats graphs as coinductive functions V -> Neighbors V where neighbors are monus-weighted neighbors (possibly infinite multisets… | ||
| Algebraic Effects Meet Hoare Logic in Cubical Agda | POPL 2024 | 2024-01-14 |
Library formalises algebraic effects with equations in Cubical Agda using quotient types instead of setoids, provides a free model plus concrete models, and… | ||
| Phases in Software Architecture | FUNARCH 2023 | 2023-09-08 |
Argues that multi‑phase program structure is captured by an applicative functor encoding phases, uses Day convolution to compose two‑phase and iterated… | ||
| Multi-phase computation as an applicative functor | TyDe 2023 | 2023-09-04 |
Claims that structuring a computation as an applicative with phases (implemented via Day convolution / an iterated, homogeneous “phases” type) lets a single… | ||
| nothing matches | ||