{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.007456488,0.001109016,0.0007281732,0.001996604,0.001310869,0.004630384,0.003499153,0.002527633,0.007429357],"category_scores_gemma":[0.01271254,0.001264272,0.003493519,0.001243798,0.007514588,0.007530077,0.005105858,0.006056181,0.002296295],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002785042,"about_ca_system_score_gemma":0.00332167,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00206456,"about_ca_topic_score_gemma":0.001435822,"domain_scores_codex":[0.991393,0.00200922,0.0008519786,0.001638118,0.002934881,0.001172939],"domain_scores_gemma":[0.9915558,0.004679098,0.000808712,0.001489796,0.001251711,0.000214848],"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.00002776201,0.00003660101,0.0001214072,0.0001190747,0.00001869609,0.0001048192,0.0002978751,0.007099833,0.001764353,0.9766873,0.0005646632,0.0131576],"study_design_scores_gemma":[0.0000648151,0.00005947218,0.00009307323,0.0001214582,0.00004711947,0.0001386398,0.00009093895,0.05142273,0.007298677,0.9252287,0.01539428,0.00004012351],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.003097111,0.00013853,0.9913768,0.0002953323,0.0000589353,0.00009570532,0.000104118,0.0008718537,0.003961685],"genre_scores_gemma":[0.20357,0.0006390452,0.7862735,0.0008315182,0.0002582402,0.0005612534,0.0006610174,0.000617422,0.006588058],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007456488,"threshold_uncertainty_score":0.03943413,"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."}}