{"id":"W4321480286","doi":"10.46298/entics.10360","title":"A Categorical Normalization Proof for the Modal Lambda-Calculus","year":2023,"lang":"en","type":"article","venue":"Electronic Notes in Theoretical Informatics and Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Simply typed lambda calculus; Church encoding; Typed lambda calculus; System F; Modal; Computer science; Lambda calculus; Programming language; Normalization (sociology); Calculus (dental); Curry–Howard correspondence; Mathematics; Algorithm; Theoretical computer science","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.00505041,0.0008906166,0.001186292,0.001604923,0.003076275,0.003478368,0.003174144,0.001619257,0.01094027],"category_scores_gemma":[0.008852139,0.001077935,0.003229326,0.002146148,0.006373329,0.01326289,0.007480878,0.008435299,0.002141379],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.005276404,"about_ca_system_score_gemma":0.004117947,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004608487,"about_ca_topic_score_gemma":0.003290405,"domain_scores_codex":[0.9956928,0.0008921378,0.0002158755,0.0009568175,0.001805299,0.0004371369],"domain_scores_gemma":[0.9957144,0.001798056,0.0001868304,0.0007675275,0.001261798,0.0002714858],"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.00001257118,0.00001488912,0.0001182333,0.00003894937,0.000007428542,0.00004693116,0.0001904615,0.0007598884,0.0007485353,0.9900079,0.001273172,0.006780939],"study_design_scores_gemma":[0.00001717812,0.00001486649,0.0001628079,0.00003507215,0.00002118287,0.00009466436,0.00007294204,0.008544852,0.002776688,0.9669797,0.02124684,0.00003315716],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0100588,0.000453636,0.9599066,0.002209093,0.0004101307,0.00008016572,0.0002946963,0.001262702,0.02532411],"genre_scores_gemma":[0.381841,0.001306231,0.5772346,0.002809736,0.0007564357,0.0007249093,0.0007393266,0.001731119,0.03285676],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01094027,"threshold_uncertainty_score":0.03828311,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01114079662424359,"score_gpt":0.2516470990599794,"score_spread":0.2405063024357358,"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."}}