Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic. Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proceedings of the ACM on Programming Languages, 7(POPL):1770-1800, January 2023. [doi]
Abstract is missing.