{"id":"W4405080277","doi":"10.1145/3707203","title":"A Layered Approach to Intensional Analysis in Type Theory","year":2024,"lang":"en","type":"article","venue":"ACM Transactions on Programming Languages and Systems","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":"Computer science; Type theory; Programming language; Normalization (sociology); Syntax; Functional programming; Data type; Metaprogramming; Theoretical computer science; Type (biology); Algorithm; Artificial intelligence","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.005895804,0.000904879,0.000870129,0.002477085,0.001746314,0.005373516,0.003078209,0.001356556,0.005152161],"category_scores_gemma":[0.007493916,0.001501944,0.003783622,0.001885189,0.00564902,0.01404426,0.007105045,0.005567353,0.00145159],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002709826,"about_ca_system_score_gemma":0.002204891,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002893912,"about_ca_topic_score_gemma":0.003159111,"domain_scores_codex":[0.9957268,0.001332636,0.0003690337,0.0006728829,0.001316636,0.0005820012],"domain_scores_gemma":[0.9953024,0.001357589,0.000313523,0.001983693,0.0007895049,0.000253347],"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.00002602839,0.00001864662,0.0003533451,0.00005675893,0.00003086376,0.00007189836,0.0005501179,0.004242665,0.002272053,0.9779158,0.0007019685,0.01375986],"study_design_scores_gemma":[0.0000124852,0.00003123422,0.0001766834,0.00006512832,0.00005126984,0.0001377456,0.00009440594,0.03761837,0.004806569,0.936444,0.02051941,0.00004266208],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.003061024,0.0001636072,0.9915715,0.000356647,0.00006584421,0.00002923087,0.00005859568,0.0005943712,0.004099116],"genre_scores_gemma":[0.156111,0.0004809568,0.8352021,0.0005717359,0.0002377713,0.0002380431,0.0001502001,0.0005921853,0.006415852],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005895804,"threshold_uncertainty_score":0.03118038,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02670016142233279,"score_gpt":0.287105682198416,"score_spread":0.2604055207760832,"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."}}