Tags

Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq

Author: Nicholas Coltharp (mail@heraplem.xyz)

Last modified: 2026-06-10 Wed 14:30

Emacs 30.2 (Org mode 9.7.11)

Validate