Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. ~ Nicolas Chappe et als. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/choice-trees-representing-and-reasoning-about-nondeterministic-recursive-and-impure-programs-in-rocq/797B95A45813CAE54CFFFA3D7B163BA4 #ITP #Rocq
