{"id":"W3005150256","doi":"10.1145/2775051.2677012","title":"Proof Spaces for Unbounded Parallelism","year":2015,"lang":"en","type":"article","venue":"ACM SIGPLAN Notices","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":8,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; Deutsche Forschungsgemeinschaft","keywords":"Computer science; Correctness; Separation logic; Mathematical proof; Soundness; Gas meter prover; Automated theorem proving; Abstract interpretation; Theoretical computer science; Programming language; Formal proof; TRACE (psycholinguistics); Hoare logic; Axiom; Mathematics","routes":{"ca_aff":true,"ca_fund":true,"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.007803345,0.001106001,0.001027001,0.001674247,0.002482833,0.004398747,0.002648069,0.001174728,0.01135793],"category_scores_gemma":[0.02141916,0.001362739,0.003165402,0.001271921,0.006088359,0.01433932,0.00831535,0.006969994,0.001805949],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002487371,"about_ca_system_score_gemma":0.002711141,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001424175,"about_ca_topic_score_gemma":0.001504745,"domain_scores_codex":[0.9905663,0.00328402,0.0007488307,0.001787157,0.003019639,0.0005940852],"domain_scores_gemma":[0.973598,0.01779519,0.001124984,0.004807727,0.002140543,0.0005336044],"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.00002762724,0.00002309335,0.0001223901,0.0001560907,0.00002977492,0.00008895748,0.0002933004,0.003816768,0.0009886957,0.979186,0.001532056,0.01373528],"study_design_scores_gemma":[0.00002155696,0.00001373029,0.00003527442,0.00004434758,0.00001623935,0.00004309442,0.00003854216,0.01525336,0.001299931,0.9695803,0.01364176,0.00001182713],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00449515,0.0005972061,0.9850383,0.001299965,0.0001429452,0.00009722631,0.0001843466,0.0011907,0.00695418],"genre_scores_gemma":[0.2235929,0.001046825,0.7633991,0.001171669,0.0004073704,0.000605779,0.0006035433,0.0009616298,0.008211275],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01135793,"threshold_uncertainty_score":0.04126853,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.07243827479088721,"score_gpt":0.2919481229640843,"score_spread":0.2195098481731971,"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."}}