{"id":"W2899165262","doi":"10.1017/s0960129518000415","title":"A case study in programming coinductive proofs: Howe’s method","year":2018,"lang":"en","type":"article","venue":"Mathematical Structures in Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Bisimulation; Coinduction; Computer science; Programming language; Operational semantics; Congruence (geometry); Theoretical computer science; Semantics (computer science); Mathematics","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":[],"consensus_categories":[],"category_scores_codex":[0.002970838,0.0002868344,0.000428101,0.0004501824,0.0002922507,0.0008001815,0.002055111,0.0000748677,0.00001055106],"category_scores_gemma":[0.0001925035,0.0002104043,0.0000543122,0.002457511,0.0006632545,0.0007775636,0.001210777,0.0003118061,0.00002157122],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001714068,"about_ca_system_score_gemma":0.0001770875,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002508592,"about_ca_topic_score_gemma":0.0003151073,"domain_scores_codex":[0.9963413,0.0002798632,0.0006015198,0.001148925,0.0008082293,0.0008201782],"domain_scores_gemma":[0.9982427,0.0002372328,0.0001579133,0.0009763444,0.0001940761,0.0001917103],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000006971046,0.0006372955,0.00740298,0.00006237577,0.000009442088,0.00369366,0.03412558,0.0001083331,0.00003773971,0.3518271,0.00001369733,0.6020749],"study_design_scores_gemma":[0.001147135,0.001076469,0.007260493,0.00003331687,0.00000806361,0.01108047,0.001245765,0.4275876,0.0005168941,0.5492446,0.0001069227,0.0006922714],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1615845,0.00001363751,0.8361177,0.00006245195,0.0005967884,0.001140696,1.325312e-7,0.0001347135,0.0003494385],"genre_scores_gemma":[0.6434786,6.490876e-8,0.3562784,0.00005225149,0.000123296,0.000055188,6.917042e-8,0.000006857687,0.000005323233],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6013826,"threshold_uncertainty_score":0.858004,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04918352910942796,"score_gpt":0.3443535858998575,"score_spread":0.2951700567904295,"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."}}