{"id":"W2512420590","doi":"10.1145/2966268.2966269","title":"Mechanizing Proofs about Mendler-style Recursion","year":2016,"lang":"en","type":"article","venue":"","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Mathematical proof; Computer science; Proof assistant; Recursion (computer science); Programming language; Normalization (sociology); Compiler; Simply typed lambda calculus; Structural proof theory; Type theory; Proof theory; Typed lambda calculus; Formal proof; Lambda calculus; Theoretical computer science; Functional programming; ENCODE; Calculus (dental); Mathematics; Type (biology)","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0003876197,0.0001101346,0.0001206436,0.00005754115,0.0001076661,0.0001202734,0.0005811781,0.00006332138,0.00009398781],"category_scores_gemma":[0.00003356536,0.00005923754,0.00005134422,0.0001835667,0.0000180228,0.000416003,0.0002027168,0.0000427127,0.000721784],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004198621,"about_ca_system_score_gemma":0.00003041374,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004396814,"about_ca_topic_score_gemma":0.00001666465,"domain_scores_codex":[0.9988759,0.0000524589,0.0001737967,0.0003560744,0.0002327413,0.0003090263],"domain_scores_gemma":[0.9992549,0.00004264912,0.00007257855,0.000466404,0.00006913106,0.00009436212],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.000001325127,0.00002229193,0.0001278235,0.000007323432,0.000005728713,0.000004883675,0.0002128054,6.073048e-8,0.003585157,0.7773692,0.001907297,0.2167561],"study_design_scores_gemma":[0.001065179,0.0004589172,0.0003597245,0.00004579733,0.00000745046,0.00006462928,0.00009648866,0.001679209,0.0747249,0.1935115,0.7273237,0.0006624898],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0005137852,0.0001358272,0.9410014,0.0009470962,0.0007601561,0.0001992188,1.784681e-7,0.0004470227,0.05599533],"genre_scores_gemma":[0.968447,0.00001325012,0.01347745,0.0001404512,0.0001162863,0.00002115568,3.289026e-7,0.000008097846,0.01777593],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9679332,"threshold_uncertainty_score":0.9277314,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0245050427859752,"score_gpt":0.2432990708912072,"score_spread":0.218794028105232,"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."}}