{"id":"W2147137665","doi":"10.1145/1389449.1389469","title":"Programming with proofs and explicit contexts","year":2008,"lang":"en","type":"article","venue":"","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":73,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Computer science; Programming language; Functional programming; Semantics (computer science); Decidability; Data type; 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.01045424,0.0007646796,0.0006920234,0.001214678,0.001948959,0.005001347,0.002191888,0.001462827,0.003809364],"category_scores_gemma":[0.01811808,0.001156003,0.001394024,0.001281183,0.007699585,0.02009825,0.007181137,0.005234906,0.0008874041],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001627659,"about_ca_system_score_gemma":0.002198491,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001098015,"about_ca_topic_score_gemma":0.001011049,"domain_scores_codex":[0.9931519,0.003197629,0.0006084471,0.001024095,0.001450804,0.0005670945],"domain_scores_gemma":[0.9844151,0.009172733,0.0007438712,0.003861838,0.001417989,0.0003885055],"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.00001199089,0.000006724853,0.00007724983,0.00004858903,0.0000056756,0.00003877271,0.0002779889,0.0008573681,0.0002752092,0.9905748,0.0003471924,0.00747854],"study_design_scores_gemma":[0.00001554935,0.00001172593,0.00003225515,0.00003761398,0.00001656554,0.00008282444,0.00006943949,0.003817386,0.001335809,0.9815381,0.01302999,0.00001278631],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01471562,0.001407341,0.9624826,0.002663417,0.0001710132,0.00004369722,0.00008677907,0.0008857968,0.01754374],"genre_scores_gemma":[0.500334,0.002207089,0.4831293,0.00110281,0.000499954,0.0002108543,0.0002241625,0.0006234359,0.01166839],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01045424,"threshold_uncertainty_score":0.05528796,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02401452591102263,"score_gpt":0.2298431368797395,"score_spread":0.2058286109687169,"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."}}