{"id":"W2995123640","doi":"10.1145/3371129","title":"Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time","year":2019,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":30,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"FP7 Ideas: European Research Council; Leverhulme Trust; McGill University; National Science Foundation","keywords":"Kleene algebra; Kleene's recursion theorem; Completeness (order theory); Algebra over a field; Equational logic; Universal algebra; Contrast (vision); Linear algebra","routes":{"ca_aff":false,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004340634,0.0001874272,0.0002888034,0.0001322309,0.00003875342,0.0001007225,0.00238695,0.00008725877,0.000007582642],"category_scores_gemma":[0.0005645776,0.0001186746,0.0000817223,0.0008728267,0.0001168209,0.0003083275,0.0004904846,0.0001966877,0.00002384988],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004059765,"about_ca_system_score_gemma":0.00004483242,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006505398,"about_ca_topic_score_gemma":0.000005414798,"domain_scores_codex":[0.9986355,0.00001705098,0.0002961516,0.0003959512,0.0003517378,0.000303564],"domain_scores_gemma":[0.9985164,0.00008089764,0.0003820599,0.0006877033,0.0002863183,0.00004663923],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"observational","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0004215805,0.001645594,0.4091183,0.0009632114,0.0002001247,0.000006496647,0.02791269,0.00002569331,0.1407635,0.04509622,0.0002773795,0.3735692],"study_design_scores_gemma":[0.007550426,0.01251039,0.2117016,0.006897179,0.0001948518,0.0001183283,0.007044197,0.01872593,0.7196263,0.007775725,0.005408423,0.002446669],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9958745,0.0001560077,0.0000752195,0.0003833738,0.00005511766,0.0007645597,8.218213e-7,0.0001666601,0.002523749],"genre_scores_gemma":[0.9615775,0.000003721006,0.0378426,0.00002993931,0.00002694571,0.00004255387,0.0000024947,0.00001849429,0.0004557606],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.5788628,"threshold_uncertainty_score":0.4839411,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01116509791335096,"score_gpt":0.2304979998718409,"score_spread":0.21933290195849,"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."}}