{"id":"W4414955533","doi":"10.1017/s0956796825100105","title":"Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq","year":2025,"lang":"en","type":"preprint","venue":"Journal of Functional Programming","topic":"Complex Systems and Decision Making","field":"Decision Sciences","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"National Science Foundation","keywords":"Nondeterministic algorithm; Bisimulation; Concurrency; Embedding; Monad (category theory); Coinduction; HOL; Denotational semantics; Leverage (statistics)","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["metaresearch","metaepi_narrow","scholarly_communication"],"consensus_categories":[],"category_scores_codex":[0.006617251,0.000411936,0.001181838,0.001386045,0.0003176989,0.001962643,0.0006545862,0.0003587945,0.00003481301],"category_scores_gemma":[0.01103279,0.0003210448,0.0003682057,0.0008477558,0.0001624968,0.000449192,0.001374322,0.001527224,0.000002272139],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001290285,"about_ca_system_score_gemma":0.0004327179,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001171118,"about_ca_topic_score_gemma":0.0002801313,"domain_scores_codex":[0.9931884,0.000411954,0.00275859,0.000973364,0.002205593,0.0004620551],"domain_scores_gemma":[0.9914939,0.003525261,0.0027944,0.0005463202,0.001375263,0.0002648424],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"observational","study_design_scores_codex":[0.0002402864,0.0001282417,0.2539001,0.0001405887,0.0001109193,0.0001845544,0.0008458655,0.001269297,0.00002108158,0.00130519,0.001403434,0.7404504],"study_design_scores_gemma":[0.003851303,0.0007876715,0.6056979,0.01425969,0.0003128851,0.002577015,0.008652318,0.03213092,0.000007622497,0.1137615,0.2165678,0.001393391],"study_design_candidate":"observational","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.8866715,0.0306921,0.06851616,0.00105678,0.007157101,0.001827651,0.00002732661,0.0000847476,0.003966583],"genre_scores_gemma":[0.9654784,0.00008445071,0.03084177,0.00007045856,0.00126575,0.00003820975,0.000004734486,0.00002718453,0.002189114],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.7390571,"threshold_uncertainty_score":0.9999242,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1625735914183837,"score_gpt":0.398653377644027,"score_spread":0.2360797862256433,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}