This extended abstract summarizes the article presented at POPL this year: "Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq" by N Chappe, P He, L Henrio, Y Zakowski, S Zdancewic - Published in Proceedings of the ACM on Programming Languages, 2023.

It introduces a new formalism designed specifically to facilitate the definition of and reasoning about nondeterministic computations in Coq's dependent type theory. The key idea is to update Xia, et al.'s interaction trees framework with native support for nondeterminisic ``choice nodes'' that represent internal choices made during computation.