{"id":"W2145575901","doi":"10.1017/s0956796810000158","title":"Formal polytypic programs and proofs","year":2010,"lang":"en","type":"article","venue":"Journal of Functional Programming","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"Trinity College","funders":"Irish Research Council; Science Foundation Ireland; Irish Research Council for Science, Engineering and Technology","keywords":"Mathematical proof; Computer science; Haskell; Programming language; Proof assistant; Lemma (botany); Function (biology); Recursion (computer science); Functional programming; 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.003048554,0.0004504482,0.0004137135,0.0008167502,0.000970318,0.002556168,0.001429442,0.0008392872,0.006116792],"category_scores_gemma":[0.008321608,0.000528147,0.0008515416,0.001021172,0.00470067,0.004414881,0.003722039,0.002438856,0.000932732],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00129905,"about_ca_system_score_gemma":0.001547829,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001697435,"about_ca_topic_score_gemma":0.001276003,"domain_scores_codex":[0.9951755,0.001757544,0.0003968825,0.0007170693,0.001466697,0.0004864297],"domain_scores_gemma":[0.9899148,0.005045155,0.0009160012,0.002376069,0.001516027,0.0002319725],"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.00005667324,0.00003377927,0.0005029279,0.0003198022,0.0000320896,0.0002997263,0.000708193,0.009150747,0.004008291,0.9456372,0.00302126,0.03622927],"study_design_scores_gemma":[0.00004070467,0.00004035818,0.0003369138,0.0001263985,0.00004196947,0.00039591,0.000209105,0.03703826,0.01506062,0.8986139,0.04805459,0.00004116006],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02000142,0.0005463509,0.9641462,0.0007780379,0.0001333714,0.000062223,0.0001683961,0.002614404,0.01154957],"genre_scores_gemma":[0.6144987,0.0009894746,0.3720463,0.0009778069,0.0002493204,0.0001914954,0.0004114027,0.00092543,0.009710094],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.006116792,"threshold_uncertainty_score":0.02046263,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02135160255679166,"score_gpt":0.2337157939823748,"score_spread":0.2123641914255831,"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."}}