Part of the beauty of this paper is that the algorithm is total and it's relatively easy to prove (and therefore to implement in Type Theory). You only need to use 3 tricks to make Agda accept the whole development (two for the code, one for an example)

· · Web · 0 · 0 · 0
Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré est un serveur Mastodon francophone, géré par La Quadrature du Net.