{"id":"W4401202381","doi":"10.1145/3704856","title":"Formal Foundations for Translational Separation Logic Verifiers","year":2025,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung; National Science Foundation","keywords":"Separation logic; Programming language; Computer science; Soundness; Automated theorem proving; Non-monotonic logic; Proof theory; Mathematical proof; Automated reasoning; Semantics (computer science); Proof assistant; Front and back ends; Theoretical 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.0004662938,0.0001270835,0.000147313,0.0001120487,0.0003051968,0.0002280426,0.001494812,0.00007609397,0.000002088057],"category_scores_gemma":[0.0005286108,0.00008885327,0.0001445601,0.0004504028,0.00006874104,0.0004433137,0.0002091127,0.00009502133,0.000002931713],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002874853,"about_ca_system_score_gemma":0.0000549634,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000132686,"about_ca_topic_score_gemma":0.000005086168,"domain_scores_codex":[0.9989834,0.000007875539,0.0002525504,0.0002637388,0.0002260984,0.0002663221],"domain_scores_gemma":[0.9991253,0.0001103871,0.0001825938,0.0003206958,0.0002322374,0.00002876055],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00001754426,0.00006156028,0.00105906,0.0001213122,0.00003422406,8.760441e-8,0.0008740158,0.00001137584,0.0007787484,0.8915104,0.0008023384,0.1047294],"study_design_scores_gemma":[0.002267896,0.0008194898,0.006278484,0.0001354577,0.0001435667,0.00001711098,0.002301292,0.005616763,0.0490406,0.7765567,0.1561444,0.0006782392],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0595312,0.0009871626,0.870805,0.02311811,0.002208027,0.005493117,0.00001018846,0.001080336,0.03676691],"genre_scores_gemma":[0.9471853,0.00000245087,0.05143234,0.0002031924,0.00006582354,0.000204702,0.000005781565,0.000006706101,0.0008937483],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8876541,"threshold_uncertainty_score":0.3623331,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02596139765242241,"score_gpt":0.3176937870598194,"score_spread":0.291732389407397,"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."}}