Post #2669083
2026-04-08 13:16 UTC
The Agda implementation of the main theorem of our paper, as well as a library we wrote for writing recursive algorithms based on coalgebras for well founded functors, can be found at https://git8.cs.fau.de/software/intrinsically-recursive/ .
In our paper we show how one can also use our technique for proving recursivity of coalgebras in a non-indexed setting, as well as providing case studies of QuickSort, CYK parsing, and the Euclidean algorithm. 7/8
Replies (2)
-
@cxandru@types.pl 2026-04-08 13:17
Next to PLDI, I will be giving a talk about this work at TYPES, and Henning Urbat will give one at CMCS, so keep your eyes peeled 👀. 8/8
-
@Taneb@hacksrus.xyz 2026-04-13 10:26
@cxandru@types.pl any reason this is using cubical for its definition of categories rather than agda-categories (which I think works better with stdlib)?