{"id":"W4406222352","doi":"10.1145/3704851","title":"A Dependent Type Theory for Meta-programming with Intensional Analysis","year":2025,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Programming language; Computer science; Type (biology); Type theory","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.001383798,0.0002951933,0.0005878338,0.0003598473,0.0002592046,0.0003485892,0.003004916,0.0001061153,0.000006267713],"category_scores_gemma":[0.001445908,0.0001607388,0.0004874491,0.002059808,0.0001442828,0.000221859,0.0008977845,0.0002055875,0.000002599335],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004714007,"about_ca_system_score_gemma":0.00006914164,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00005609938,"about_ca_topic_score_gemma":0.00002544666,"domain_scores_codex":[0.9980083,0.00003110922,0.0003805982,0.0006206803,0.0004924384,0.0004669104],"domain_scores_gemma":[0.9975978,0.000325002,0.0003874835,0.0008648867,0.0007552147,0.00006958187],"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.0002087564,0.0002766718,0.006846264,0.0003091719,0.006670037,0.000003456066,0.001257981,0.00002833334,0.0005801132,0.8230005,0.0005000492,0.1603187],"study_design_scores_gemma":[0.007366178,0.007127183,0.009894297,0.000596286,0.0486513,0.0001865891,0.02120228,0.003927364,0.1692483,0.5175061,0.2100281,0.004266047],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2248679,0.01579467,0.7064571,0.0176087,0.002969718,0.01373613,0.00002202557,0.003664523,0.01487924],"genre_scores_gemma":[0.914991,0.000004704103,0.08249886,0.0002923669,0.00004679513,0.0004365366,0.000003153183,0.00001779125,0.001708796],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.6901231,"threshold_uncertainty_score":0.6554737,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02565928138098042,"score_gpt":0.2842653169020579,"score_spread":0.2586060355210775,"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."}}